Type checking dependent (record) types and subtyping

Abstract

In this work we put forward an algorithm for the mechanical verification of an extension of Martin-Löf's theory of types with dependent record types and subtyping. We first give a concise description of that theory and motivate its use for the formalization of algebraic constructions. Then we concentrate on the informal explanation and specification of a proof checker that we have implemented. The logical heart of this proof checker is a type checking algorithm for the forms of judgement of a particular formulation of the extended theory which incorporates a notion of parameter. The algorithm has been proven sound with respect to the latter calculus. We include a discussion on that proof in the present work.