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.
Get full access to this article
View all access options for this article.