Computational interpretations of logics

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.