First Steps Towards Cumulative Inductive Types in CIC

DOI10.1007/978-3-319-25150-9_36zbMath1471.03022OpenAlexW2401046173MaRDI QIDQ2787453

Bart Jacobs, Amin Timany

Publication date: 25 February 2016

Published in: Theoretical Aspects of Computing - ICTAC 2015 (Search for Journal in Brave)

Full work available at URL: https://lirias.kuleuven.be/handle/123456789/513812

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Type theory (03B38)

Related Items (2)

Cumulative Inductive Types in Coq ⋮ Ornaments for Proof Reuse in Coq

Uses Software

• Unnamed Item

This page was built for publication: First Steps Towards Cumulative Inductive Types in CIC