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.
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.
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.
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.
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.
Rodolphe Lepigre & Christophe Raffalli (2016):
Implementation of the SubML language.
Available at https://github.com/rlepigre/subml.
Rodolphe Lepigre & Christophe Raffalli (2017):
Implementation of the PML_2 proof system.
Available at https://github.com/rlepigre/pml.
Frank Pfenning & Conal Elliott (1988):
Higher-Order Abstract Syntax.
In: PLDI.
ACM,
pp. 199–208.
Available at https://doi.org/10.1145/960116.54010.
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.
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.
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.
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.
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.