Explicit universes for the calculus of constructions

DOI10.1007/3-540-45685-6_9MaRDI QIDQ4484336zbMATH OpenFDO

Authors Judicaël Courant

Publication date 12 June 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2410/24100115.htm

Mathematics Subject Classification ID

Recommendations

• Type checking with universes
• The implicit calculus of constructions. extending pure type systems with an intersection type binder and subtyping
• scientific article; zbMATH DE number 4191621
• A calculus of constructions with explicit subtyping
• A higher-order calculus and theory abstraction

Cited in

(9)

• A compact kernel for the calculus of inductive constructions
• Type checking with universes
• A higher-order calculus and theory abstraction
• Universe polymorphism in Coq
• A Computational Approach to an Alternative Working Environment for the Constructible Universe
• Universal constructions in umbral calculus
• More on implicit syntax
• The Implicit Calculus of Constructions as a Programming Language with Dependent Types
• Computer theorem proving in mathematics

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Explicit universes for the calculus of constructions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4484336)