The Completeness of Typing for Context-Semantics

Issue title: Typed Lambda Calculi and Applications 2005, Selected Papers

Article type: Research Article

Authors: Coquand, Thierry

Affiliations: Department of Computer Science, Chalmers University of Technology, Göteborg, Sweden. E-mail: coquand@cs.chalmers.se

Abstract: We present a variation of Hindley's completeness theorem for simply typed λ-calculus. It is based on a Kripke semantics where the worlds are contexts, called context-semantics. This variation was obtained indirectly by simplifying an analysis of a fragment of polymorphic λ-calculus [2]. We relate in this way works done in proof theory [4,14] with a fundamental result in λ-calculus.

Journal: Fundamenta Informaticae, vol. 77, no. 4, pp. 293-301, 2007