On semantics of a term calculus for classical logic (Q2929866)
From MaRDI portal
 | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: On semantics of a term calculus for classical logic |
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | On semantics of a term calculus for classical logic |
scientific article |
Statements
On semantics of a term calculus for classical logic (English)
0 references
14 November 2014
0 references
lambda calculus
0 references
confluence
0 references
continuation semantics
0 references
Two subcalculi of the calculus introduced by Curien and Herbelin to provide the Curry-Howard correspondence for classical logic are investigated. One of these subcalculi corresponds to the ``call by value'' and the other to the ``call by name'' paradigm. A proof of confluence is given and soundness theorems are proven for both variants. A thorough overview of the work on continuation semantics is given.
0 references
