A Formalised Proof of the Soundness and Completeness of a Simply Typed Lambda-Calculus with Explicit Substitutions

Catarina Coquand. A Formalised Proof of the Soundness and Completeness of a Simply Typed Lambda-Calculus with Explicit Substitutions. Higher-Order and Symbolic Computation, 15(1):57-90, 2002.

Abstract

Abstract is missing.