The fundamental connection between logic and computation, known as the Curry–Howard correspondence or formulae-as-types and proofs-as-programs paradigm, relates logical and computational systems. We present an overview of computational interpretations of intuitionistic and classical logic: • intuitionistic natural deduction - λ-calculus • intuitionistic sequent calculus - λGtz-calculus • classical natural deduction - λµ-calculus • classical sequent calculus - λµµ~-calculus. In this work we summarise the authors’ contributions in this field. Fundamental properties of these calculi, such as confluence, normalisation properties, reduction strategies call-by-value and call-by-name, separability, reducibility method, λ-models are in focus. These fundamental properties and their counterparts in logics, via the Curry– Howard correspondence, are discussed.

Computational Interpretations of Logics

LIKAVEC, Silvia
2009-01-01

Abstract

The fundamental connection between logic and computation, known as the Curry–Howard correspondence or formulae-as-types and proofs-as-programs paradigm, relates logical and computational systems. We present an overview of computational interpretations of intuitionistic and classical logic: • intuitionistic natural deduction - λ-calculus • intuitionistic sequent calculus - λGtz-calculus • classical natural deduction - λµ-calculus • classical sequent calculus - λµµ~-calculus. In this work we summarise the authors’ contributions in this field. Fundamental properties of these calculi, such as confluence, normalisation properties, reduction strategies call-by-value and call-by-name, separability, reducibility method, λ-models are in focus. These fundamental properties and their counterparts in logics, via the Curry– Howard correspondence, are discussed.
2009
12(20)
159
215
http://elib.mi.sanu.ac.rs/files/journals/zr/20/n020p159.pdf
Silvia Ghilezan; Silvia Likavec
File in questo prodotto:
File Dimensione Formato  
Silviae_4aperto.pdf

Accesso aperto

Tipo di file: POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione 559.54 kB
Formato Adobe PDF
559.54 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2318/90204
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact