Article contents
Type checking dependent (record) types and subtyping
Published online by Cambridge University Press: 01 March 2000
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.
- Type
- Research Article
- Information
- Copyright
- © 2000 Cambridge University Press
- 2
- Cited by
Discussions
No Discussions have been published for this article.