|Title:||Computational interpretations of logics||Journal:||Zbornik Radova||Volume:||12||Issue:||20||First page:||159||Last page:||215||Issue Date:||2009||Rank:||M14||URL:||http://elib.mi.sanu.ac.rs/files/journals/zr/20/n020p159.pdf||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.
|Publisher:||Mathematical Institute of the SASA|
Show full item record
checked on Nov 28, 2022
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.