@inproceedings{CGO-2011-Leroy,
	acmid         = "2190048",
	author        = "Xavier Leroy",
	booktitle     = "{Proceedings of the Ninth International Symposium on Code Generation and Optimization}",
	doi           = "10.1109/CGO.2011.5764668",
	isbn          = "978-1-61284-356-8",
	publisher     = "{IEEE Computer Society}",
	title         = "{Formally verifying a compiler: Why? How? How far?}",
	year          = 2011,
}