@inproceedings{timany-2018-cumulative,
  doi = {10.4230/LIPICS.FSCD.2018.29},
  url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.29},
  author = {Timany, Amin and Sozeau, Matthieu},
  keywords = {Coq, Proof Assistants, Inductive Types, Universes, Cumulativity},
  language = {en},
  title = {Cumulative Inductive Types In Coq},
  volume = {108},
  pages = {29:1-29:16},
  publisher = {Schloss Dagstuhl – Leibniz-Zentrum für Informatik},
  year = {2018},
  copyright = {Creative Commons Attribution 3.0 Unported license},
  booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}
}