From Self-Interpreters to Normalization by Evaluation - Mathieu Boespflug (CoRR, 2009)

Conversion by Evaluation. - Mathieu Boespflug (PADL, 2010)

Full Reduction at Full Throttle. - Mathieu Boespflug; Maxime Dénès; Benjamin Grégoire (CPP, 2011)

Multi-level Contextual Type Theory - Mathieu Boespflug; Brigitte Pientka (LFMTP, 2011)

Conception d'un noyau de vérification de preuves pour le λΠ-calcul modulo. (Design and implementation of a proof verifying kernel for the λΠ-calculus modulo). - Mathieu Boespflug (2011)

CoqInE: Translating the Calculus of Inductive Constructions into the λΠ-calculus Modulo. - Mathieu Boespflug; Guillaume Burel (PxTP, 2012)

The λΠ-calculus Modulo as a Universal Proof Language. - Mathieu Boespflug; Quentin Carbonneaux; Olivier Hermant (PxTP, 2012)

Linear Haskell: practical linearity in a higher-order polymorphic language. - Jean-Philippe Bernardy; Mathieu Boespflug; Ryan R. Newton; Simon Peyton Jones; Arnaud Spiwack (Proc. ACM Program. Lang., 2018)