Cumulative inductive types in Coq

Amin Timany, Matthieu Sozeau, and Bart Jacobs: Cumulative inductive types in Coq. In TYPES'17, May 2017.
.pdf [slides] .pdf
Unpublished Workshop Paper
The bibtex source for this publication:
@inproceedings{Types17,
  author = {Amin Timany and Matthieu Sozeau and Bart Jacobs},
  title = {{Cumulative inductive types in Coq}},
  booktitle = {Types},
  year = {2017},
  month = {May},
  url = {http://types2017.elte.hu}
}