Universe Polymorphism in Coq

DOI10.1007/978-3-319-08970-6_32zbMath1416.68179OpenAlexW1875842672MaRDI QIDQ2879272

Nicolas Tabareau, Matthieu Sozeau

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

Related Items (6)

Unnamed Item ⋮ A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading ⋮ Cumulative Inductive Types in Coq ⋮ Categoricity results and large model constructions for second-order ZF in dependent type theory ⋮ Heterogeneous Substitution Systems Revisited ⋮ Generate & Check Method for Verifying Transition Systems in CafeOBJ

Uses Software

• Coq

This page was built for publication: Universe Polymorphism in Coq