scientific article; zbMATH DE number 1927418

MaRDI QIDQ4484336zbMATH OpenFDO

Authors Judicaël Courant

Publication date 12 June 2003

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
• scientific article; zbMATH DE number 1722663
• 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
• scientific article; zbMATH DE number 1182848 (Why is no real title available?)
• scientific article; zbMATH DE number 1765684 (Why is no real title available?)
• 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:

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