The extended calculus of constructions (ECC) with inductive types

DOI10.1016/0890-5401(92)90031-AzbMath0784.03009MaRDI QIDQ1193601

Christian-Emil Ore

Publication date: 27 September 1992

Published in: Information and Computation (Search for Journal in Brave)

zbMATH Keywords

inductive typesExtended Calculus of Constructionshigher order functional calculuspredicative cumulative type hierarchy

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Related Items

Program specification and data refinement in type theory, Constructive sets in computable sets, Semantics of constructions. I: The traditional approach, Inductive types and exact completion, Semantics of constructions. II: The initial algebraic approach, Least and greatest fixed points in intuitionistic natural deduction, Structures definable in polymorphism

Uses Software

• LEGO

Cites Work

• The system \({\mathcal F}\) of variable types, fifteen years later
• The calculus of constructions
• A small complete category
• Fundamentals of contemporary set theory
• A higher-order calculus and theory abstraction
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item