The Girard Translation Extended with Recursion

Torben BraŁner

February 1995


This paper extends Curry-Howard interpretations of Intuitionistic Logic (IL) and Intuitionistic Linear Logic (ILL) with rules for recursion. The resulting term languages, the tex2html_wrap_inline24-calculus and the linear tex2html_wrap_inline24-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 tex2html_wrap_inline24-calculus into terms of the linear tex2html_wrap_inline24-calculus is induced via the extended Curry-Howard isomorphisms. This embedding is shown to be sound with respect to the categorical interpretations.

Available as PostScript, PDF, DVI.


Last modified: 2003-06-08 by webmaster.