1. Ali Assaf, Guillaume Burel, Raphaël Cauderlier, David Delahaye, Gilles Dowek, Catherine Dubois, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant & Ronan Saillard (2018): Expressing theories in the λΠ-calculus modulo theory and in the Dedukti system. Available at Submitted paper.
  2. N.G de Bruijn (1972): Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae (Proceedings) 75(5), pp. 381 – 392. Available at
  3. Arthur Charguéraud (2012): The Locally Nameless Representation. J. Autom. Reasoning 49(3), pp. 363–408. Available at
  4. Adam Chlipala (2008): Parametric higher-order abstract syntax for mechanized semantics. In: ICFP. ACM, pp. 143–156. Available at
  5. Christophe Raffalli (1995): A Normaliser for Pure and Typed λ-Calculus. Available at First version implemented in Caml Light.
  6. Christophe Raffalli (2007): PML: a new proof assistant. Available at Prototype implementation.
  7. André Hirschowitz & Marco Maggesi (2012): Nested Abstract Syntax in Coq. J. Autom. Reasoning 49(3), pp. 409–426. Available at
  8. Rodolphe Lepigre (2017): Lambdapi: a new implementation of Dedukti. Available at
  9. Rodolphe Lepigre (2017): Semantics and Implementation of an Extension of ML for Proving Programs. (Sémantique et Implantation d'une Extension de ML pour la Preuve de Programmes). Grenoble Alpes University, France.
  10. Rodolphe Lepigre & Christophe Raffalli (2016): Implementation of the SubML language. Available at
  11. Rodolphe Lepigre & Christophe Raffalli (2017): Implementation of the PML_2 proof system. Available at
  12. Frank Pfenning & Conal Elliott (1988): Higher-Order Abstract Syntax. In: PLDI. ACM, pp. 199–208. Available at
  13. Andrew M. Pitts & Mark R. Shinwell (2008): Generative Unbinding of Names. Logical Methods in Computer Science 4(1). Available at
  14. François Pottier (2005): Cαml. Available at
  15. François Pottier (2006): An overview of Cαml. In: ACM Workshop on ML, Electronic Notes in Theoretical Computer Science 148, pp. 27–52. Available at
  16. Rodolphe Lepigre and Christophe Raffalli (2015): The Bindlib OCaml Library Version 5. Available at May be installed using the Opam package manager.
  17. Rodolphe Lepigre and Christophe Raffalli (2017-2018): Practical Subtyping for Curry-Style Languages. Available at Under revision for publication in the TOPLAS journal.
  18. Mark R. Shinwell (2006): Fresh O'Caml: Nominal Abstract Syntax for the Masses. Electr. Notes Theor. Comput. Sci. 148(2), pp. 53–77. Available at
  19. Mark R. Shinwell, Andrew M. Pitts & Murdoch James Gabbay (2003): FreshML: programming with binders made simple. SIGPLAN Notices 38(9), pp. 263–274. Available at

Comments and questions to:
For website issues: