An Algorithm for Type-Checking Dependent Types

We present a simple type-checker for a language with dependent types and let expressions, with a simple proof of correctness. Introduction Type Theory provides an interesting approach to the problem of (interactive) proof-checking. Instead of introducing, like in LCF [10], an abstract data type of theorems, it uses the proofs-as-programs analogy and reduces the problem of proof checking to the problem of type-checking in a programming language with dependent types [5]. This approach presents several advantages, well described in [11,5], among those being the possibility of independent proof verification and of a uniform treatment for naming constants and theorems. It is crucial however for this approach to proof-checking to have a simple and reliable type-checking algorithm. Since the core part of such languages, like the ones described in [5,7], seems very simple, there may be some hope for such a short and simple type-checker for dependent types. Indeed, de Bruijn sketches such an al..