Higher-Order and Symbolic Computation, 15(1)57-90
A Formalised Proof of the Soundness and Completeness of a Simply Typed Lambda-Calculus with Explicit SubstitutionsCatarina Coquand, Department of Computing Science, Chalmers University of Technology and University of Göteborg, 412 96 Göteborg, Sweden
|
Abstract: We present a simply-typed lambda-calculus with
explicit substitutions and we give a fully formalised proof of its
soundness and completeness with respect to Kripke models. We further
give conversion rules for the calculus and show also for them that
they are sound and complete with respect to extensional equality in
the Kripke model. A decision algorithm for conversion is given and
proven correct. We use the technique "normalisation by evaluation" in
order to prove these results. An important aspect of this work is that
it is not a formalisation of an existing proof, instead the proof has
been done in interaction with the proof system, ALF.
Keywords: formal methods, type theory, explicit substitutions, normalisation |
This article can be downloaded [here].
![[picture of journal cover]](../LISP.JPG)