[Prev][Next][Index][Thread]

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

> 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.