Mathieu Boespflug, Staged computation in types. Submitted. October 2012.
[ .pdf, .pdf (with proofs) ]
Mathieu Boespflug and Guillaume Burel.
CoqInE: translating the calculus of inductive constructions into
the lambda-pi-calculus modulo.
In Proceedings of the Second International Workshop on Proof
Exchange for Theorem Proving, volume 878 of CEUR Workshop
Proceedings, pages 44–50, Manchester, UK, June 2012.
[ bib |
.pdf ]
Mathieu Boespflug, Quentin Carbonneaux, and Olivier Hermant.
The lambda-pi-calculus modulo as a universal proof language.
In Proceedings of the Second International Workshop on Proof
Exchange for Theorem Proving, volume 878 of CEUR Workshop
Proceedings, pages 28–43, Manchester, UK, June 2012.
[ bib |
.pdf ]
Mathieu Boespflug and Brigitte Pientka.
Multi-level contextual type theory.
In Proceedings Sixth International Workshop on Logical
Frameworks and Meta-languages: Theory and Practice, October 2011.
EPTCS 71, 2011, pp. 29-43.
[ bib |
DOI |
http ]
Mathieu Boespflug.
Conception d'un noyau de vérification de preuves pour le
lambda-Pi-calcul modulo.
PhD thesis, École Polytechnique, Palaiseau, January 2011.
[ bib |
.pdf ]
Mathieu Boespflug, Maxime Dénès, and Benjamin Grégoire.
Full reduction at full throttle.
In Jean-Pierre Jouannaud and Zhong Shao, editors, Certified
Programs and Proofs, volume 7086 of Lecture Notes in Computer Science,
pages 362–377, 2011.
[ bib |
DOI |
.pdf ]
Mathieu Boespflug.
Conversion by evaluation.
In Proceedings of the Twelfth Internation Symposium on Pracical
Aspects of Declarative Languages, Madrid, Spain, January 2010.
A preliminary version was presented at the NbE'09 workshop.
[ bib |
DOI |
.pdf ]
Mathieu Boespflug.
From self-interpreters to normalization by evaluation.
In Informal Proceedings of the 2009 Workshop on Normalization by
Evaluation, pages 29–34, Los Angeles, California, August 2009.
[ bib |
.pdf ]
Mathieu Boespflug.
TaiChi: how to check your types with serenity.
In Wouter Swierstra, editor, The Monad.Reader, volume 9,
pages 17–31. November 2007.
[ bib |
.pdf ]
Talks
2012-01-20 McGill Graduate Seminar: First class reflection for shorter proofs
[slides]
2011-08-26 LFMTP 2011: Multi-level contextual type theory
[slides]
2011-07-26 Rewinding the stack for parsing and pretty printing
[slides]
