Lambda Calculus with Explicit Substitution as a term assignment?

• To: types@cis.upenn.edu
• Subject: Lambda Calculus with Explicit Substitution as a term assignment?
• From: Sanjiva Prasad <sanjiva@brics.dk>
• Date: Mon, 21 Sep 1998 15:05:32 +0200 (MET DST)

Hi:

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.

Thanks,
sanjiva@brics.dk

• Prev: top down type inferece
• Next: An efficient implementation of type inference with subtyping
• Index(es):
  • Main
  • Thread