Proof-term synthesis on dependent-type systems via explicit substitutions

Typed lambda -terms are used as a compact and linear representation of proo fs in intuitionistic logic. This is possible since the Curry-Howard isomorp hism relates proof-trees with typed lambda -terms. The proofs-as-terms prin ciple can be used to verify the validity of a proof by type checking the la mbda -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, eve ry construction step, not just the last one, may be type checked. The metho d is based on a suitable calculus where substitutions as well as meta-varia bles are first-class objects. (C) 2001 Elsevier Science B.V. All rights res erved.