Since 2014
The Girard Translation Extended with Recursion
BRICS Report Series
View Archive Info| Field | Value | |
| Title |
The Girard Translation Extended with Recursion
|
|
| Creator |
Braüner, Torben
|
|
| Description |
This paper extends Curry-Howard interpretations of Intuitionistic Logic (IL) and Intuitionistic Linear Logic (ILL) with rules for recursion. The resulting term languages, the rec-calculus and the linear rec-calculus respectively, are given soundcategorical interpretations. The embedding of proofs of IL into proofs of ILL given by the Girard Translation is extended with the rules for recursion, such that an embedding of terms of the rec-calculus into terms of the linear rec-calculus is induced via the extended Curry-Howard isomorphisms. This embedding is shown to be sound with respect to the categorical interpretations.Full version of paper to appear in Proceedings of CSL '94, LNCS 933, 1995.
|
|
| Publisher |
Aarhus University
|
|
| Contributor |
—
|
|
| Date |
1995-01-13
|
|
| Type |
info:eu-repo/semantics/article
info:eu-repo/semantics/publishedVersion — |
|
| Format |
application/pdf
|
|
| Identifier |
https://tidsskrift.dk/brics/article/view/19882
10.7146/brics.v2i13.19882 |
|
| Source |
BRICS Report Series; No 13 (1995): RS-13 The Girard Translation Extended with Recursion
BRICS Report Series; No 13 (1995): RS-13 The Girard Translation Extended with Recursion 1601-5355 0909-0878 |
|
| Language |
eng
|
|
| Relation |
https://tidsskrift.dk/brics/article/view/19882/17535
|
|
| Rights |
Copyright (c) 2015 BRICS Report Series
|
|