@article(DBLP:journals/corr/AnandM17,
 author       = {Abhishek Anand and Greg Morrisett},
 year         = {2017},
 title        = {Revisiting Parametricity: Inductives and Uniformity of Propositions},
 journal      = {CoRR},
 volume       = {abs/1705.01163},
 url          = {http://arxiv.org/abs/1705.01163},
)
@inproceedings(Aydemir2005,
 author       = {B. Aydemir and A. Bohannon and M. Fairbairn and N. Foster and B. Pierce and P. Sewell and D. Vytiniotis and G. Washburn and S. Weirich and S. Zdancewic},
 year         = {2005},
 title        = {Mechanized Metatheory for the Masses: The PoplMark Challenge},
 booktitle    = {Proceedings of TPHOLs'05},
 publisher    = {Springer-Verlag},
 pages        = {50--65},
 doi          = {10.1007/11541868_4},
)
@book(bar:84,
 author       = {Hendrik Barendregt},
 year         = {1984},
 title        = {The \ensuremath{\lambda}-calculus Its Syntax and Semantics},
 edition      = {revised},
 series       = {Studies in Logic and the Foundations of Mathematics},
 volume       = {103},
 publisher    = {North Holland},
 doi          = {10.2307/2274112},
)
@article(Benke:2003,
 author       = {Marcin Benke and Peter Dybjer and Patrik Jansson},
 year         = {2003},
 title        = {Universes for Generic Programs and Proofs in Dependent Type Theory},
 journal      = {Nordic Journal of Computing},
 volume       = {10},
 number       = {4},
 pages        = {265--289},
 url          = {http://dl.acm.org/citation.cfm?id=985799.985801},
)
@inproceedings(Cheney,
 author       = {James Cheney},
 year         = {2005},
 title        = {Scrap Your Nameplate: (Functional Pearl)},
 booktitle    = {Proceedings of the Tenth ACM SIGPLAN International Conference on Functional Programming},
 series       = {ICFP '05},
 publisher    = {ACM},
 address      = {New York, NY, USA},
 pages        = {180--191},
 doi          = {10.1145/1086365.1086389},
)
@inproceedings(Copello:LSFA17,
 author       = {Ernesto Copello and Nora Szasz and {\'A}lvaro Tasistro},
 year         = {2017 in press},
 title        = {Machine-checked proof of the Church-Rosser Theorem for the Lambda Calculus using the Barendregt Variable Convention in Constructive Type Theory},
 booktitle    = {LSFA 2017},
 url          = {http://lsfa2017.cic.unb.br/LSFA2017.pdf},
)
@article(CopelloTSBF16,
 author       = {Ernesto Copello and \IeC{\'A}lvaro Tasistro and Nora Szasz and Ana Bove and Fern\IeC{\'a}ndez, Maribel},
 year         = {2016},
 title        = {Alpha-Structural Induction and Recursion for the \ensuremath{\lambda}-calculus in Constructive Type Theory},
 journal      = {ENTCS},
 volume       = {323},
 pages        = {109 -- 124},
 doi          = {10.1016/j.entcs.2016.06.008},
)
@article(Delaware:2013:MLC,
 author       = {Benjamin Delaware and Bruno C. d. S. Oliveira and Tom Schrijvers},
 year         = {2013},
 title        = {Meta-theory \`{a} La Carte},
 journal      = {SIGPLAN Not.},
 volume       = {48},
 number       = {1},
 pages        = {207--218},
 doi          = {10.1145/2429069.2429094},
)
@article(GP02:newapproach,
 author       = {Murdoch J. Gabbay and Andrew M. Pitts},
 year         = {2001},
 title        = {A New Approach to Abstract Syntax with Variable Binding},
 journal      = {Formal Aspects of Computing},
 volume       = {13},
 number       = {3\IeC{\textemdash}5},
 pages        = {341\IeC{\textemdash}363},
 doi          = {10.1007/s001650200016},
)
@inbook(Lee2012,
 author       = {Gyesik Lee and Bruno Oliveira and Sungkeun Cho and Kwangkeun Yi},
 year         = {2012},
 title        = {GMeta: A Generic Formal Metatheory Framework for First-Order Representations},
 publisher    = {Springer},
 doi          = {10.1.1.298.2957},
)
@inproceedings(licata-harper-09,
 author       = {Daniel R. Licata and Robert Harper},
 year         = {2009},
 title        = {A universe of binding and computation},
 booktitle    = {International Conference on Functional Programming (ICFP)},
 pages        = {123--134},
 doi          = {10.1145/1596550.1596571},
)
@book(mlof84:bibliopolis,
 author       = {Martin-L{\"o}f, Per},
 year         = {1984},
 title        = {Intuitionistic type theory},
 series       = {Studies in Proof Theory. Lecture Notes},
 volume       = {1},
 publisher    = {Naples},
)
@inproceedings(Morris:2004,
 author       = {Peter Morris and Thorsten Altenkirch and Conor McBride},
 year         = {2006},
 title        = {Exploring the Regular Tree Types},
 booktitle    = {International Conference on Types for Proofs and Programs},
 series       = {TYPES'04},
 publisher    = {Springer-Verlag},
 address      = {Berlin, Heidelberg},
 doi          = {10.1007/11617990_16},
)
@inproceedings(Norell2009,
 author       = {Ulf Norell},
 year         = {2009},
 title        = {Dependently Typed Programming in Agda},
 booktitle    = {Proceedings of the 6th International Conference on Advanced Functional Programming},
 series       = {AFP'08},
 publisher    = {Springer-Verlag},
 address      = {Berlin},
 doi          = {10.1145/1481861.1481862},
)
@book(Pierce:2002,
 author       = {Benjamin C. Pierce},
 year         = {2002},
 title        = {Types and Programming Languages},
 edition      = {1st},
 publisher    = {The MIT Press},
)
@article(SHINWELL200653,
 author       = {Mark R. Shinwell},
 year         = {2006},
 title        = {Fresh O'Caml: Nominal Abstract Syntax for the Masses},
 journal      = {ENTCS},
 volume       = {148},
 number       = {2},
 doi          = {10.1016/j.entcs.2005.11.040},
)
@article(ShinwellPG03,
 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},
 doi          = {10.1145/944746.944729},
)
@incollection(UrbanT05,
 author       = {Christian Urban and Christine Tasson},
 year         = {2005},
 title        = {{Nominal Techniques in Isabelle/HOL}},
 booktitle    = {Automated Deduction \IeC{\textendash} CADE-20},
 series       = {LNCS},
 volume       = {3632},
 publisher    = {Springer Berlin Heidelberg},
 doi          = {10.1007/s10817-008-9097-2},
)
@article(YOSHIDA200773,
 author       = {Nobuko Yoshida and Vasco T. Vasconcelos},
 year         = {2007},
 title        = {Language Primitives and Type Discipline for Structured Communication-Based Programming Revisited: Two Systems for Higher-Order Session Communication},
 journal      = {ENTCS},
 volume       = {171},
 number       = {4},
 pages        = {73 -- 93},
 doi          = {10.1016/j.entcs.2007.02.056},
)