Re: Lambda Calculus with Explicit Substitution as a term assignment?
To: firstname.lastname@example.org (Sanjiva Prasad)
Subject: Re: Lambda Calculus with Explicit Substitution as a term assignment?
From: Rene Vestergaard <email@example.com>
Date: Wed, 23 Sep 1998 14:10:16 +0100 (BST)
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
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.
PS! I noticed, Sanjiva, that you are at BRICS. Olivier Danvy should be
able to give you further information on these issues.
 J. Zucker: "The Correspondence between Cut-Elimination and
Normalization, Part I". Annals of Mathematical Logic, 7:1-112
 G. Pottinger: "Normalization as a Homomorphic Image of
Cut-Elimination". Annals of Mathematical Logic, 12:323-357
 G. Mints: "Normal Forms for Sequent Derivations". In P. Odifreddi
(ed.): "Kreiseliana --- about and around Georg Kreisel" (1996).
A.K. Peters Publishers.