Authors: Ghilezan, Silvia 
Likavec, Silvia
Title: Computational interpretations of logics
Journal: Zbornik Radova
Volume: 12
Issue: 20
First page: 159
Last page: 215
Issue Date: 2009
Rank: M14
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

Page view(s)

checked on May 9, 2024

Google ScholarTM


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.