Type checking in the presence of meta-variables

Ulf Norell and Catarina Coquand. Type checking in the presence of meta-variables. Submitted to TLCA, january 2007.
[pdf]

In this paper we present a type checking algorithm for a dependently typed logical framework extended with meta-variables. It is common for such frameworks to accept that unification creates substitutions that are not well typed, but we give a novel approach to the treatment of meta-variables where well-typedness of substitutions is guaranteed. To ensure type correctness the type checker creates an optimal well-typed approximation of the term being type checked. We use a restricted form of pattern unification, but we believe that the results carry over to other unification algorithms. We prove that the algorithm is sound and terminating. The proposed algorithm has been implemented with promising results.


Valid HTML 4.01! Disclaimer
Last modified: Thu Jan 4 15:38:20 2007