• People
• Events
• Research

A Unifying Theory of Dependent Types: the Schematic Approach

Abstract:Presented is a theory of dependent types, which unifies coherently Martin-Lof's type theory with universes and Coquand-Huet's Calculus of Constructions and can be seen as an extension of the Extended Calculus of Constructions by a large class of inductive data types. This is a further development of the idea to enhance in type theory a conceptual distinction between the notions of logical formula (proposition) and data type, and is another step aiming at the development of a unifying language for modular development of programs, specifications, and profits.

LFCS report ECS-LFCS-92-202