A Type-Checking Algorithm for Martin-Loef Type Theory with Subtyping Based on Normalisation by Evaluation

摘要

We present a core Martin-Loef type theory with subtyping; it has a cumulative hierarchy of universes and the contravariant rule for subtyping between dependent product types. We extend to this calculus the normalisation by evaluation technique defined for a variant of MLTT without subtyping. This normalisation function makes the subtyping relation and type-checking decidable. To our knowledge, this is the first time that the normalisation by evaluation technique has been considered in the context of subtypes, which introduce some subtleties in the proof of correctness of NbE; an important result to prove correctness and completeness of type-checking.