References

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 http://www.lsv.fr/~dowek/Publi/expressing.pdf. 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 https://doi.org/10.1016/1385-7258(72)90034-0.
3. Arthur Charguéraud (2012): The Locally Nameless Representation. J. Autom. Reasoning 49(3), pp. 363–408. Available at https://doi.org/10.1007/s10817-011-9225-2.
4. Adam Chlipala (2008): Parametric higher-order abstract syntax for mechanized semantics. In: ICFP. ACM, pp. 143–156. Available at http://doi.acm.org/10.1145/1411204.1411226.
5. Christophe Raffalli (1995): A Normaliser for Pure and Typed λ-Calculus. Available at https://lama.univ-savoie.fr/~raffalli/normaliser.html. First version implemented in Caml Light.
6. Christophe Raffalli (2007): PML: a new proof assistant. Available at http://lama.univ-savoie.fr/~raffalli/pml. Prototype implementation.
7. André Hirschowitz & Marco Maggesi (2012): Nested Abstract Syntax in Coq. J. Autom. Reasoning 49(3), pp. 409–426. Available at https://doi.org/10.1007/s10817-010-9207-9.
8. Rodolphe Lepigre (2017): Lambdapi: a new implementation of Dedukti. Available at https://github.com/rlepigre/lambdapi.
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 https://github.com/rlepigre/subml.
11. Rodolphe Lepigre & Christophe Raffalli (2017): Implementation of the PML_2 proof system. Available at https://github.com/rlepigre/pml.
12. Frank Pfenning & Conal Elliott (1988): Higher-Order Abstract Syntax. In: PLDI. ACM, pp. 199–208. Available at https://doi.org/10.1145/960116.54010.
13. Andrew M. Pitts & Mark R. Shinwell (2008): Generative Unbinding of Names. Logical Methods in Computer Science 4(1). Available at https://doi.org/10.2168/LMCS-4(1:4)2008.
14. François Pottier (2005): Cαml. Available at http://gallium.inria.fr/~fpottier/alphaCaml/.
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 http://gallium.inria.fr/~fpottier/publis/fpottier-alphacaml.pdf.
16. Rodolphe Lepigre and Christophe Raffalli (2015): The Bindlib OCaml Library Version 5. Available at https://github.com/rlepigre/ocaml-bindlib. May be installed using the Opam package manager.
17. Rodolphe Lepigre and Christophe Raffalli (2017-2018): Practical Subtyping for Curry-Style Languages. Available at http://lepigre.fr/files/docs/lepigre2017_subml.pdf. 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 https://doi.org/10.1016/j.entcs.2005.11.040.
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 http://doi.acm.org/10.1145/944746.944729.

Comments and questions to: eptcs@eptcs.org

For website issues: webmaster@eptcs.org