@ARTICLE {
	AUTHOR = "Meven Lennon-Bertrand and Kenji Maillard and Nicolas Tabareau and {\'E}ric Tanter",
	TITLE ="Gradualizing the Calculus of Inductive Constructions",
	JOURNAL = "ACM Transactions on Programming Languages and Systems (TOPLAS)",
	VOLUME = "44",
	NUMBER = "2",
	PAGES = "7:1-7:82",
	MONTH = "Jun",
	YEAR = "2022",
	PUBLISHER = "ACM Press",
	ADDRESS = "New York, NY, USA",
	ISSN = "0164-0925"
	}