% Bibliography downloaded from https://researchr.org/downloadbibtex/bibliography/variable-binding/compact

@inproceedings{WeirichYS11,
  title = {Binders unbound},
  author = {Stephanie Weirich and Brent A. Yorgey and Tim Sheard},
  year = {2011},
  doi = {10.1145/2034773.2034818},
  url = {http://doi.acm.org/10.1145/2034773.2034818},
  researchr = {https://researchr.org/publication/WeirichYS11},
  cites = {0},
  citedby = {0},
  pages = {333-345},
  booktitle = {ICFP},
}

@article{BellegardeH94,
  title = {Substitution: A Formal Methods Case Study Using Monads and Transformations},
  author = {Françoise Bellegarde and James Hook},
  year = {1994},
  tags = {case study, transformation},
  researchr = {https://researchr.org/publication/BellegardeH94},
  cites = {0},
  citedby = {0},
  journal = {SCP},
  volume = {23},
  number = {2-3},
  pages = {287-311},
}

@inproceedings{PouillardP10,
  title = {A fresh look at programming with names and binders},
  author = {Nicolas Pouillard and François Pottier},
  year = {2010},
  doi = {10.1145/1863543.1863575},
  url = {http://doi.acm.org/10.1145/1863543.1863575},
  tags = {programming},
  researchr = {https://researchr.org/publication/PouillardP10},
  cites = {0},
  citedby = {0},
  pages = {217-228},
  booktitle = {ICFP},
}

@inproceedings{NeronTVW15,
  title = {A Theory of Name Resolution},
  author = {Pierre Néron and Andrew P. Tolmach and Eelco Visser and Guido Wachsmuth},
  year = {2015},
  doi = {10.1007/978-3-662-46669-8_9},
  url = {http://dx.doi.org/10.1007/978-3-662-46669-8_9},
  researchr = {https://researchr.org/publication/NeronTVW15},
  cites = {0},
  citedby = {0},
  pages = {205-231},
  booktitle = {ESOP},
}

@article{GabbayP02,
  title = {A New Approach to Abstract Syntax with Variable Binding},
  author = {Murdoch Gabbay and Andrew M. Pitts},
  year = {2002},
  url = {http://link.springer.de/link/service/journals/00165/bibs/2013003/20130341.htm},
  tags = {abstract syntax, variable binding, systematic-approach},
  researchr = {https://researchr.org/publication/GabbayP02},
  cites = {0},
  citedby = {0},
  journal = {fac},
  volume = {13},
  number = {3-5},
  pages = {341-363},
}

@inproceedings{Ricciotti15,
  title = {Binding Structures as an Abstract Data Type},
  author = {Wilmer Ricciotti},
  year = {2015},
  doi = {10.1007/978-3-662-46669-8_31},
  url = {http://dx.doi.org/10.1007/978-3-662-46669-8_31},
  researchr = {https://researchr.org/publication/Ricciotti15},
  cites = {0},
  citedby = {0},
  pages = {762-786},
  booktitle = {ESOP},
}

@article{deBruijn72,
  title = {Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the {Church-Rosser} theorem},
  author = {N. G. de Bruijn},
  year = {1972},
  researchr = {https://researchr.org/publication/deBruijn72},
  cites = {0},
  citedby = {0},
  journal = {Indagationes Mathematicae},
  volume = {34},
  number = {5},
  pages = {381-392},
}

@inproceedings{PfenningE88,
  title = {Higher-Order Abstract Syntax},
  author = {Frank Pfenning and Conal Elliott},
  year = {1988},
  doi = {10.1145/960116.54010},
  url = {https://doi.org/10.1145/960116.54010},
  tags = {abstract syntax},
  researchr = {https://researchr.org/publication/PfenningE88},
  cites = {0},
  citedby = {0},
  pages = {199-208},
  booktitle = {PLDI},
}

@inproceedings{Chlipala08,
  title = {Parametric higher-order abstract syntax for mechanized semantics},
  author = {Adam J. Chlipala},
  year = {2008},
  doi = {10.1145/1411204.1411226},
  url = {http://doi.acm.org/10.1145/1411204.1411226},
  tags = {semantics, abstract syntax},
  researchr = {https://researchr.org/publication/Chlipala08},
  cites = {0},
  citedby = {0},
  pages = {143-156},
  booktitle = {ICFP},
}

@article{Chargueraud12,
  title = {The Locally Nameless Representation},
  author = {Arthur Charguéraud},
  year = {2012},
  doi = {10.1007/s10817-011-9225-2},
  url = {http://dx.doi.org/10.1007/s10817-011-9225-2},
  researchr = {https://researchr.org/publication/Chargueraud12},
  cites = {0},
  citedby = {0},
  journal = {JAR},
  volume = {49},
  number = {3},
  pages = {363-408},
}

@inproceedings{BernardyP13,
  title = {Names for free: polymorphic views of names and binders},
  author = {Jean-Philippe Bernardy and Nicolas Pouillard},
  year = {2013},
  doi = {10.1145/2503778.2503780},
  url = {http://doi.acm.org/10.1145/2503778.2503780},
  researchr = {https://researchr.org/publication/BernardyP13},
  cites = {0},
  citedby = {0},
  pages = {13-24},
  booktitle = {haskell},
}

@inproceedings{McKinnaP93,
  title = {Pure Type Systems Formalized},
  author = {James McKinna and Robert Pollack},
  year = {1993},
  tags = {type system},
  researchr = {https://researchr.org/publication/McKinnaP93},
  cites = {0},
  citedby = {0},
  pages = {289-305},
  booktitle = {tlca},
}

@inproceedings{Pouillard11,
  title = {Nameless, painless},
  author = {Nicolas Pouillard},
  year = {2011},
  doi = {10.1145/2034773.2034817},
  url = {http://doi.acm.org/10.1145/2034773.2034817},
  researchr = {https://researchr.org/publication/Pouillard11},
  cites = {0},
  citedby = {0},
  pages = {320-332},
  booktitle = {ICFP},
}

@article{McBride2018,
  title = {Everybody's Got To Be Somewhere},
  author = {Conor McBride},
  year = {2018},
  month = {Jul},
  doi = {10.4204/eptcs.275.6},
  url = {http://dx.doi.org/10.4204/EPTCS.275.6},
  researchr = {https://researchr.org/publication/McBride2018},
  cites = {0},
  citedby = {0},
  journal = {Electronic Proceedings in Theoretical Computer Science},
  volume = {275},
  pages = {53-69},
}

@article{AntwerpenPRV18,
  title = {Scopes as types},
  author = {Hendrik van Antwerpen and Casper Bach Poulsen and Arjen Rouvoet and Eelco Visser},
  year = {2018},
  doi = {10.1145/3276484},
  url = {https://doi.org/10.1145/3276484},
  researchr = {https://researchr.org/publication/AntwerpenPRV18},
  cites = {0},
  citedby = {0},
  journal = {PACMPL},
  volume = {2},
  number = {OOPSLA},
}

@inproceedings{ShinwellPG03,
  title = {FreshML: programming with binders made simple},
  author = {Mark R. Shinwell and Andrew M. Pitts and Murdoch Gabbay},
  year = {2003},
  doi = {10.1145/944705.944729},
  url = {http://doi.acm.org/10.1145/944705.944729},
  tags = {programming},
  researchr = {https://researchr.org/publication/ShinwellPG03},
  cites = {0},
  citedby = {0},
  pages = {263-274},
  booktitle = {ICFP},
}

@article{Pitts03,
  title = {Nominal logic, a first order theory of names and binding},
  author = {Andrew M. Pitts},
  year = {2003},
  doi = {10.1016/S0890-5401(03)00138-X},
  url = {http://dx.doi.org/10.1016/S0890-5401(03)00138-X},
  tags = {logic},
  researchr = {https://researchr.org/publication/Pitts03},
  cites = {0},
  citedby = {0},
  journal = {iandc},
  volume = {186},
  number = {2},
  pages = {165-193},
}

@inproceedings{KonatVKWV2012,
  title = {The {Spoofax} Name Binding Language},
  author = {Gabriël Konat and Vlad A. Vergu and Lennart C. L. Kats and Guido Wachsmuth and Eelco Visser},
  year = {2012},
  doi = {10.1145/2384716.2384748},
  url = {https://doi.org/10.1145/2384716.2384748},
  tags = {C++, Spoofax},
  researchr = {https://researchr.org/publication/KonatVKWV2012},
  cites = {0},
  citedby = {0},
  booktitle = {Companion to the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2011, part of SPLASH 2012, Tucson, AR, USA, October 19 - 26, 2012},
}

@article{RouvoetAPKV20,
  title = {Knowing when to ask: sound scheduling of name resolution in type checkers derived from declarative specifications},
  author = {Arjen Rouvoet and Hendrik van Antwerpen and Casper Bach Poulsen and Robbert Krebbers and Eelco Visser},
  year = {2020},
  doi = {10.1145/3428248},
  url = {https://doi.org/10.1145/3428248},
  researchr = {https://researchr.org/publication/RouvoetAPKV20},
  cites = {0},
  citedby = {0},
  journal = {PACMPL},
  volume = {4},
  number = {OOPSLA},
}

@article{AllaisA0MM18,
  title = {A type and scope safe universe of syntaxes with binding: their semantics and proofs},
  author = {Guillaume Allais and Robert Atkey and James Chapman and Conor McBride and James McKinna},
  year = {2018},
  doi = {10.1145/3236785},
  url = {https://doi.org/10.1145/3236785},
  researchr = {https://researchr.org/publication/AllaisA0MM18},
  cites = {0},
  citedby = {0},
  journal = {PACMPL},
  volume = {2},
  number = {ICFP},
}

@inproceedings{AydemirCPPW08,
  title = {Engineering formal metatheory},
  author = {Brian E. Aydemir and Arthur Charguéraud and Benjamin C. Pierce and Randy Pollack and Stephanie Weirich},
  year = {2008},
  doi = {10.1145/1328438.1328443},
  url = {http://doi.acm.org/10.1145/1328438.1328443},
  tags = {programming languages, optimization, object-oriented programming, Machanized Metatheory, proof assistant, pattern language, type soundness, exceptions, Coq, variable binding, language engineering, Cofinite quantification, principles, little language, C++, metatheory, programming, subject-oriented programming, Syntactic type soundness, program optimization, systematic-approach, feature-oriented programming, Locally nameless},
  researchr = {https://researchr.org/publication/AydemirCPPW08},
  cites = {0},
  citedby = {0},
  pages = {3-15},
  booktitle = {POPL},
}

@article{Pottier06,
  title = {An overview of {C$\alpha$ml}},
  author = {François Pottier},
  year = {2006},
  doi = {10.1016/j.entcs.2005.11.039},
  url = {http://dx.doi.org/10.1016/j.entcs.2005.11.039},
  tags = {C++},
  researchr = {https://researchr.org/publication/Pottier06},
  cites = {0},
  citedby = {0},
  journal = {ENTCS},
  volume = {148},
  number = {2},
  pages = {27-52},
}

@article{UrbanPG04,
  title = {Nominal unification},
  author = {Christian Urban and Andrew M. Pitts and Murdoch Gabbay},
  year = {2004},
  doi = {10.1016/j.tcs.2004.06.016},
  url = {http://dx.doi.org/10.1016/j.tcs.2004.06.016},
  researchr = {https://researchr.org/publication/UrbanPG04},
  cites = {0},
  citedby = {0},
  journal = {TCS},
  volume = {323},
  number = {1-3},
  pages = {473-497},
}

@phdthesis{hal-3916,
  title = {Namely, Painless: A unifying approach to safe programming with first-order syntax with binders. (Une approche unifiante pour programmer sûrement avec de la syntaxe du premier ordre contenant des lieurs)},
  author = {Nicolas Pouillard},
  year = {2012},
  url = {https://tel.archives-ouvertes.fr/tel-00759059},
  researchr = {https://researchr.org/publication/hal-3916},
  cites = {0},
  citedby = {0},
  school = {Paris Diderot University, France},
}