Proof-term synthesis on dependent-type systems via explicit substitutions
Typed lambda -terms are used as a compact and linear representation of proofs in intuitionistic logic. This is possible since the Curry-Howard isomorphism relates proof-trees with typed lambda -terms. The proofs-as-terms principle can be used to verify the validity of a proof by type checking the lambda -term extracted from the complete proof-tree. In this paper we present a proof synthesis method for dependent-type systems where typed open terms are built incrementally at the same time as proofs are done. This way, every construction step, not just the last one, may be type checked. The method is based on a suitable calculus where substitutions as well as meta-variables are first-class objects. (C) 2001 Elsevier Science B.V. All rights reserved.
explicit substitutions proof synthesis higher-order unification lambda calculus