Computational Interpretations of Logics

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.