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 / Silvia Ghilezan; Silvia Likavec. - In: ZBORNIK RADOVA. - ISSN 0351-9406. - 12(20)(2009), pp. 159-215.
Titolo: | Computational Interpretations of Logics | |
Autori Riconosciuti: | ||
Autori: | Silvia Ghilezan; Silvia Likavec | |
Data di pubblicazione: | 2009 | |
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. | |
Volume: | 12(20) | |
Pagina iniziale: | 159 | |
Pagina finale: | 215 | |
URL: | http://elib.mi.sanu.ac.rs/files/journals/zr/20/n020p159.pdf | |
Rivista: | ZBORNIK RADOVA | |
Appare nelle tipologie: | 03A-Articolo su Rivista |
File in questo prodotto:
File | Descrizione | Tipologia | Licenza | |
---|---|---|---|---|
Silviae_4aperto.pdf | POSTPRINT (VERSIONE FINALE DELL’AUTORE) | Open Access Visualizza/Apri |