Typed Lambda Calculi and Applications
Lecture Notes in Computer Science, 1997, Volume 1210/1997, 373-389, DOI: 10.1007/3-540-62688-3_47

Inhabitation in typed lambda-calculi (a syntactic approach)

Pawel Urzyczyn

View Related Documents

Abstract

A type is inhabited (non-empty) in a typed calculus iff there is a closed term of this type. The inhabitation (emptiness) problem is to determine if a given type is inhabited. This paper provides direct, purely syntactic proofs of the following results: the inhabitation problem is PSPACE-complete for simply typed lambda-calculus and undecidable for the polymorphic second-order and higher-order lambda calculi (systems F and Fohgr).
This work was partly supported by NSF grant CCR-9417382, KBN Grant 8 T11C 034 10 and by ESPRIT BRA7232 ldquoGentzenrdquo.

Fulltext Preview

Image of the first page of the fulltext document