@unpublished(dedukti,
 author       = {Ali Assaf and Guillaume Burel and Rapha\IeC{\"e}l Cauderlier and David Delahaye and Gilles Dowek and Catherine Dubois and Fr\IeC{\'e}d\IeC{\'e}ric Gilbert and Pierre Halmagrand and Olivier Hermant and Ronan Saillard},
 year         = {2018},
 title        = {{Expressing theories in the $\lambda$$\Pi$-calculus modulo theory and in the Dedukti system}},
 url          = {http://www.lsv.fr/~dowek/Publi/expressing.pdf},
 note         = {Submitted paper},
)
@article(debruijn,
 author       = {N.G de Bruijn},
 year         = {1972},
 title        = {Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem},
 journal      = {Indagationes Mathematicae (Proceedings)},
 volume       = {75},
 number       = {5},
 pages        = {381 -- 392},
 url          = {https://doi.org/10.1016/1385-7258(72)90034-0},
)
@article(nameless,
 author       = {Chargu\IeC{\'e}raud, Arthur},
 year         = {2012},
 title        = {The Locally Nameless Representation},
 journal      = {J. Autom. Reasoning},
 volume       = {49},
 number       = {3},
 pages        = {363--408},
 url          = {https://doi.org/10.1007/s10817-011-9225-2},
)
@inproceedings(phoas,
 author       = {Adam Chlipala},
 year         = {2008},
 title        = {Parametric higher-order abstract syntax for mechanized semantics},
 booktitle    = {{ICFP}},
 publisher    = {{ACM}},
 pages        = {143--156},
 url          = {http://doi.acm.org/10.1145/1411204.1411226},
)
@misc(normaliser,
 author       = {{Christophe Raffalli}},
 year         = {1995},
 title        = {{A Normaliser for Pure and Typed $\lambda$-Calculus}},
 url          = {https://lama.univ-savoie.fr/~raffalli/normaliser.html},
 note         = {First version implemented in Caml Light},
)
@misc(pml,
 author       = {{Christophe Raffalli}},
 year         = {2007},
 title        = {{PML: a new proof assistant}},
 url          = {http://lama.univ-savoie.fr/~raffalli/pml},
 note         = {Prototype implementation},
)
@article(nested,
 author       = {Andr{\'{e}} Hirschowitz and Marco Maggesi},
 year         = {2012},
 title        = {Nested Abstract Syntax in Coq},
 journal      = {J. Autom. Reasoning},
 volume       = {49},
 number       = {3},
 pages        = {409--426},
 url          = {https://doi.org/10.1007/s10817-010-9207-9},
)
@misc(lambdapi,
 author       = {Rodolphe Lepigre},
 year         = {2017},
 title        = {{Lambdapi: a new implementation of Dedukti}},
 url          = {https://github.com/rlepigre/lambdapi},
)
@phdthesis(phd,
 author       = {Rodolphe Lepigre},
 year         = {2017},
 title        = {Semantics and Implementation of an Extension of {ML} for Proving Programs. (S\IeC{\'e}mantique et Implantation d'une Extension de {ML} pour la Preuve de Programmes)},
 school       = {Grenoble Alpes University, France},
)
@misc(subml,
 author       = {Rodolphe Lepigre and Christophe Raffalli},
 year         = {2016},
 title        = {{Implementation of the SubML language}},
 url          = {https://github.com/rlepigre/subml},
)
@misc(pml2,
 author       = {Rodolphe Lepigre and Christophe Raffalli},
 year         = {2017},
 title        = {{Implementation of the PML$_2$} proof system},
 url          = {https://github.com/rlepigre/pml},
)
@inproceedings(hoas,
 author       = {Frank Pfenning and Conal Elliott},
 year         = {1988},
 title        = {Higher-Order Abstract Syntax},
 booktitle    = {{PLDI}},
 publisher    = {{ACM}},
 pages        = {199--208},
 url          = {https://doi.org/10.1145/960116.54010},
)
@article(fresh3,
 author       = {Andrew M. Pitts and Mark R. Shinwell},
 year         = {2008},
 title        = {Generative Unbinding of Names},
 journal      = {Logical Methods in Computer Science},
 volume       = {4},
 number       = {1},
 url          = {https://doi.org/10.2168/LMCS-4(1:4)2008},
)
@misc(alphacaml,
 author       = {Fran\IeC{\c c}ois Pottier},
 year         = {2005},
 title        = {{C$\alpha$ml}},
 url          = {http://gallium.inria.fr/~fpottier/alphaCaml/},
)
@inproceedings(alphacamlpaper,
 author       = {Fran\IeC{\c c}ois Pottier},
 year         = {2006},
 title        = {An overview of {C$\alpha$ml}},
 booktitle    = {ACM Workshop on ML},
 series       = {Electronic Notes in Theoretical Computer Science},
 volume       = {148},
 pages        = {27--52},
 url          = {http://gallium.inria.fr/~fpottier/publis/fpottier-alphacaml.pdf},
)
@misc(bindlib,
 author       = {{Rodolphe Lepigre and Christophe Raffalli}},
 year         = {2015},
 title        = {{The Bindlib OCaml Library Version 5}},
 url          = {https://github.com/rlepigre/ocaml-bindlib},
 note         = {May be installed using the Opam package manager},
)
@unpublished(toplas,
 author       = {{Rodolphe Lepigre and Christophe Raffalli}},
 year         = {2017-2018},
 title        = {{Practical Subtyping for Curry-Style Languages}},
 url          = {http://lepigre.fr/files/docs/lepigre2017_subml.pdf},
 note         = {Under revision for publication in the TOPLAS journal},
)
@article(fresh2,
 author       = {Mark R. Shinwell},
 year         = {2006},
 title        = {Fresh O'Caml: Nominal Abstract Syntax for the Masses},
 journal      = {Electr. Notes Theor. Comput. Sci.},
 volume       = {148},
 number       = {2},
 pages        = {53--77},
 url          = {https://doi.org/10.1016/j.entcs.2005.11.040},
)
@article(fresh1,
 author       = {Mark R. Shinwell and Andrew M. Pitts and Murdoch James Gabbay},
 year         = {2003},
 title        = {FreshML: programming with binders made simple},
 journal      = {{SIGPLAN} Notices},
 volume       = {38},
 number       = {9},
 pages        = {263--274},
 url          = {http://doi.acm.org/10.1145/944746.944729},
)