zbMATH — the first resource for mathematics

Inductive definitions in the system Coq; rules and properties. (English) Zbl 0844.68073
Bezem, Marc (ed.) et al., Typed Lambda calculi and applications. International conference, TLCA ’93, March 16-18, 1993, Utrecht, the Netherlands. Proceedings. Berlin: Springer-Verlag. Lect. Notes Comput. Sci. 664, 328-345 (1993).
Summary: In the pure calculus of constructions, it is possible to represent data structures and predicates using higher-order quantification. However, this representation is not satisfactory, from the point of view of both the efficiency of the underlying programs and the power of the logical system. For these reasons, the calculus was extended with a primitive notion of inductive definitions. This paper describes the rules for inductive definitions in the system Coq. They are general enough to be seen as one formulation of adding inductive definitions to a typed lambda-calculus. We prove strong normalization for a subsystem of Coq corresponding to the pure calculus of constructions plus inductive definitions with only weak eliminations.
For the entire collection see [Zbl 0866.00038].

68Q45 Formal languages and automata
68Q55 Semantics in the theory of computing
ALF; Coq; LEGO; Nuprl