Computational Interrpretations of Logics


Silvia Ghilezan, Silvia Likavec




The fundamental connection between logic and computation, known as the Curry-Howard correspondence or formulae-astypes 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 - A-calculus; - intuitionistic sequent calculus - A Gtz-calculus; - classical natural deduction - AJ.L-calculus; - classical sequent calculus - XJ.Lj:L-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, A-models are in focus. These fundamental properties and their counterparts in logics, via the CurryHoward correspondence, are discussed.