[Prev][Next][Index][Thread]
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 propositionsastypes, programsasproofs account where a
lambdacalculus 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