Computational Interrpretations of Logics
Zbornik radova, Tome 12 (2009) no. 20, p. 159
Voir la notice de l'article provenant de la source eLibrary of Mathematical Institute of the Serbian Academy of Sciences and Arts
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.
@article{ZR_2009_12_20_a4,
author = {Silvia Ghilezan and Silvia Likavec},
title = {Computational {Interrpretations} of {Logics}},
journal = {Zbornik radova},
pages = {159 },
publisher = {mathdoc},
volume = {12},
number = {20},
year = {2009},
language = {en},
url = {http://geodesic.mathdoc.fr/item/ZR_2009_12_20_a4/}
}
Silvia Ghilezan; Silvia Likavec. Computational Interrpretations of Logics. Zbornik radova, Tome 12 (2009) no. 20, p. 159 . http://geodesic.mathdoc.fr/item/ZR_2009_12_20_a4/