@inproceedings{allais-2017-type, series={CPP ’17}, title={Type-and-scope safe programs and their proofs}, url={http://dx.doi.org/10.1145/3018610.3018613}, DOI={10.1145/3018610.3018613}, booktitle={Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs}, publisher={ACM}, author={Allais, Guillaume and Chapman, James and McBride, Conor and McKinna, James}, year={2017}, month=Jan, pages={195–207}, collection={CPP ’17} }