Universe polymorphism in Coq

DOI10.1007/978-3-319-08970-6_32MaRDI QIDQ2879272zbMATH OpenOpenAlexFDO

Authors Matthieu Sozeau, Nicolas Tabareau

Publication date 8 September 2014

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-08970-6_32

Mathematics Subject Classification ID

Recommendations

• Cumulative inductive types in Coq
• scientific article; zbMATH DE number 1927418
• First steps towards cumulative inductive types in CIC
• Type checking with universes
• scientific article; zbMATH DE number 1302063

Cited in

(14)

• Categoricity results and large model constructions for second-order ZF in dependent type theory
• First steps towards cumulative inductive types in CIC
• Heterogeneous substitution systems revisited
• Cumulative inductive types in Coq
• Generate \& check method for verifying transition systems in CafeOBJ
• Category theory in Coq 8.5
• A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading
• scientific article; zbMATH DE number 7649967 (Why is no real title available?)
• Generalized universe hierarchies and first-class universe levels
• Sharing proofs with predicative theories through universe-polymorphic elaboration
• Encoding Agda programs using rewriting
• Correct and complete type checking and certified erasure for \textsc{Coq}, in \textsc{Coq}
• Touring the MetaCoq project
• The Rewster: type preserving rewrite rules for the Rocq Prover. Extended version of the ITP 2024 paper

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Universe polymorphism in Coq

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