Open AccessThe Girard Translation Extended with Recursion
Author(s) -
Torben Braüner
Publication year - 1995
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v2i13.19882
Subject(s) - intuitionistic logic , mathematics , embedding , recursion (computer science) , mathematical proof , calculus (dental) , minimal logic , linear logic , curry–howard correspondence , natural deduction , discrete mathematics , algebra over a field , type theory , sequent calculus , pure mathematics , computer science , type (biology) , algorithm , programming language , zeroth order logic , description logic , dentistry , artificial intelligence , ecology , multimodal logic , biology , geometry , medicine
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 sound categorical 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.