Abstract:
This paper extends Curry-Howard interpretations of
Intuitionistic Logic (IL) and Intuitionistic Linear Logic (ILL) with rules
for recursion. The resulting term languages, the 
-calculus and
the linear -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 -calculus into terms of the linear
-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.