Publications

Shrink Fast Correctly!, O. Savary Bélanger and Andrew Appel. Principles and Practice of Declarative Programming (PPDP), to appear.

CertiCoq: A verified compiler for Coq, A. Anand, A. Appel, G. Morrisett, Z. Paraskevopoulou, R. Pollack, O. Savary Bélanger, M. Sozeau and M. Weaver. Workshop on Coq for Programming Languages (CoqPL), January 2017.

Programming type-safe transformations using higher-order abstract syntax, O. Savary Bélanger, S. Monnier and B. Pientka. Journal of Formalized Reasoning (JFR), December 2015.

Automatically Deriving Schematic Theorems for Dynamic Contexts, O. Savary Bélanger and K. Chaudhuri. Logical Frameworks and Meta-languages: Theory and Practice (LFMTP), July 2014.

Programming type-safe transformations using higher-order abstract syntax, O. Savary Bélanger, S. Monnier and B. Pientka. Certified Programs and Proofs (CPP), December 2013.