@INPROCEEDINGS {
	AUTHOR = "{\'E}ric Tanter and Nicolas Tabareau",
	TITLE = "Gradual Certified Programming in Coq",
	BOOKTITLE = "11th Dynamic Languages Symposium (DLS)",
	PAGES = "26-40",
	MONTH = "Oct",
	YEAR = "2015",
	ADDRESS = "Pittsburg, USA",
	PUBLISHER = "ACM Press",
	}