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.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.