Typing Algorithm in Type Theory with Inheritance

Abstract

We propose and study a new typing algorithm for dependent type theory. This new algorithm typechecks more terms by using inheritance between classes. This inheritance mechanism turns out to be powerful: it supports multiple inheritance, classes with parameters and uses new abstract classes FUNCLASS and SORTCLASS (respectively classes of functions and sorts). We also defines classes as records, particularily suitable for the formal development of mathematical theories. This mechanism, implemented in the proof checker Coq, can be adapted to all typed -calculus. 1 Introduction In the last years, proof checkers based on type theory appeared as convincing systems to formalize mathematics (especially constructive mathematics) and to prove correctness of software and hardware. In a proof checker, one can interactively build definitions, statements and proofs. The system is then able to check automatically whether the definitions are well-formed and the proofs are correct. Modern systems ar...