# Re: Lambda Calculus with Explicit Substitution as a term assignment?

• Subject: Re: Lambda Calculus with Explicit Substitution as a term assignment?
• From: Rene Vestergaard <jrvest@cee.hw.ac.uk>
• Date: Wed, 23 Sep 1998 14:10:16 +0100 (BST)
• Cc: types@cis.upenn.edu
• In-Reply-To: <199809211311.JAA20459@saul.cis.upenn.edu> from "Sanjiva Prasad" at Sep 21, 98 03:05:32 pm

> Is there a propositions-as-types, programs-as-proofs account where a
> lambda-calculus with explicit substitution serves as the term
> assignment language for a suitable intuitionistic logic?  Any pointers
> to relevant papers will be appreciated.

Yes. I recently wrote a technical report entitled "The Cut Rule and
Explicit Substitutions" in which I construct such calculi from known
logical deduction style inference systems. It essentially shows that
there is a tight connection between propagation of the cut rule(s) and
propagation of explicit substitutions a la \s, \t, and \xgc.  It also
has quite a few references to earlier work that addresses similar (but
not the same!) issues. It is available from

http://www.cee.hw.ac.uk/~jrvest/Writings/writings.html

In a forthcoming article (tentatively called "The Correspondence
between Cut-Propagation, Explicit Substitutions, and \beta-reduction")
I prove how a variant of the Zucker-Pottinger(-Mints) epimorphism
[1,2,3] factors through explicit substitutions. That is, I prove that
\s and \t (and \xgc?) can be obtained as homomorphic images of cut
propagation. These calculi with explicit substitution produce, in
turn, \beta-reduction as a homomorphic image.

Regards
/R

PS! I noticed, Sanjiva, that you are at BRICS. Olivier Danvy should be
able to give you further information on these issues.

[1] J. Zucker: "The Correspondence between Cut-Elimination and
Normalization, Part I". Annals of Mathematical Logic, 7:1-112
(1974). North-Holland.

[2] G. Pottinger: "Normalization as a Homomorphic Image of
Cut-Elimination". Annals of Mathematical Logic, 12:323-357
(1977). North-Holland.

[3] G. Mints: "Normal Forms for Sequent Derivations". In P. Odifreddi
(ed.): "Kreiseliana --- about and around Georg Kreisel" (1996).
A.K. Peters Publishers.

`