@misc(cmu:twelf,
 author       = "M. Ashley-Rollman and K. Crary and R. Harper",
 title        = "A solution to the POPLmark Challenge",
)
@article(DBLP:journals/jar/AvronHMP92,
 author       = "A. Avron and F. Honsell and I. A. Mason and R. Pollack",
 year         = "1992",
 title        = "Using Typed Lambda Calculus to Implement Formal Systems on a Machine",
 journal      = "J. Autom. Reasoning",
 volume       = "9",
 number       = "3",
 pages        = "309--354",
 url          = "http://dx.doi.org/10.1007/BF00245294",
)
@inproceedings(poplmark,
 author       = "B. E. Aydemir\ et al.",
 year         = "2005",
 title        = "Mechanized Metatheory for the Masses: The PoplMark Challenge",
 editor       = "Joe Hurd and Thomas F. Melham",
 booktitle    = "TPHOLs",
 series       = "Lecture Notes in Computer Science",
 volume       = "3603",
 publisher    = "Springer",
 pages        = "50--65",
 url          = "http://dx.doi.org/10.1007/11541868_4",
)
@misc(poplmark:url,
 author       = "B. E. Aydemir\ et al.",
 title        = "The POPLmark Challenge",
 url          = "http://www.seas.upenn.edu/~plclub/poplmark/",
)
@article(DBLP:journals/jfp/BucaloHMSH06,
 author       = "A. Bucalo and F. Honsell and M. Miculan and I. Scagnetto and M. Hofmann",
 year         = "2006",
 title        = "Consistency of the theory of contexts",
 journal      = "J. Funct. Program.",
 volume       = "16",
 number       = "3",
 pages        = "327--372",
 url          = "http://dx.doi.org/10.1017/S0956796806005892",
)
@misc(chargueraud:coq,
 author       = "A. Chargu{\'e}raud",
 title        = "A solution to the POPLmark Challenge",
)
@article(chargueraud-11-ln,
 author       = "A. Chargu{\'e}raud",
 year         = "2011",
 title        = "The Locally Nameless Representation",
 journal      = "Journal of Automated Reasoning",
 pages        = "1--46",
 url          = "http://dx.doi.org/10.1007/s10817-011-9225-2",
)
@misc(chlipala:coq,
 author       = "A. Chlipala",
 title        = "A solution to the POPLmark Challenge",
)
@inproceedings(DBLP:conf/lpar/CiaffaglioneLM03,
 author       = "A. Ciaffaglione and L. Liquori and M. Miculan",
 year         = "2003",
 title        = "Imperative Object-Based Calculi in Co-inductive Type Theories",
 editor       = "Moshe Y. Vardi and Andrei Voronkov",
 booktitle    = "LPAR",
 series       = "Lecture Notes in Computer Science",
 volume       = "2850",
 publisher    = "Springer",
 pages        = "59--77",
 url          = "http://dx.doi.org/10.1007/978-3-540-39813-4_4",
)
@inproceedings(DBLP:conf/icfp/CiaffaglioneLM03,
 author       = "A. Ciaffaglione and L. Liquori and M. Miculan",
 year         = "2003",
 title        = "Reasoning on an imperative object-based calculus in Higher Order Abstract Syntax",
 booktitle    = "MERLIN",
 publisher    = "ACM",
 pages        = "1--10",
 url          = "http://doi.acm.org/10.1145/976571.976574",
)
@article(DBLP:journals/jar/CiaffaglioneLM07,
 author       = "A. Ciaffaglione and L. Liquori and M. Miculan",
 year         = "2007",
 title        = "Reasoning about Object-based Calculi in (Co)Inductive Type Theory and the Theory of Contexts",
 journal      = "J. Autom. Reasoning",
 volume       = "39",
 number       = "1",
 pages        = "1--47",
 url          = "http://dx.doi.org/10.1007/s10817-006-9061-y",
)
@misc(alberto:url,
 author       = "A. Ciaffaglione and I. Scagnetto",
 year         = "2012",
 title        = "A solution to the POPLmark Challenge",
)
@article(coquandCC,
 author       = "T. Coquand and G. P. Huet",
 year         = "1988",
 title        = "The Calculus of Constructions",
 journal      = "Inf. Comput.",
 volume       = "76",
 number       = "2/3",
 pages        = "95--120",
 url          = "http://dx.doi.org/10.1016/0890-5401(88)90005-3",
)
@inproceedings(DBLP:conf/tlca/DespeyrouxFH95,
 author       = "J. Despeyroux and A. P. Felty and A. Hirschowitz",
 year         = "1995",
 title        = "Higher-Order Abstract Syntax in Coq",
 editor       = "Mariangiola Dezani-Ciancaglini and Gordon D. Plotkin",
 booktitle    = "TLCA",
 series       = "Lecture Notes in Computer Science",
 volume       = "902",
 publisher    = "Springer",
 pages        = "124--138",
 url          = "http://dx.doi.org/10.1007/BFb0014049",
)
@misc(fairbairn:alpha,
 author       = "M. Fairbairn",
 title        = "A solution to the POPLmark Challenge",
)
@article(DBLP:journals/fac/GabbayP02,
 author       = "M. Gabbay and A. M. Pitts",
 year         = "2002",
 title        = "A New Approach to Abstract Syntax with Variable Binding",
 journal      = "Formal Asp. Comput.",
 volume       = "13",
 number       = "3-5",
 pages        = "341--363",
 url          = "http://dx.doi.org/10.1007/s001650200016",
)
@misc(gacek:abella,
 author       = "A. Gacek",
 title        = "A solution to the POPLmark Challenge",
)
@phdthesis(gacek:phd,
 author       = "A. Gacek",
 year         = "2009",
 title        = "A Framework for Specifying, Prototyping, and Reasoning about Computational Systems",
 school       = "University of Minnesota",
)
@inproceedings(DBLP:conf/lics/HarperHP87,
 author       = "R. Harper and F. Honsell and G. D. Plotkin",
 year         = "1987",
 title        = "A Framework for Defining Logics",
 booktitle    = "LICS",
 publisher    = "IEEE Computer Society",
 pages        = "194--204",
)
@misc(hirsch-mag:coq,
 author       = "A. Hirschowitz and M. Maggesi",
 title        = "A solution to the POPLmark Challenge",
)
@article(DBLP:journals/jar/HirschowitzM12,
 author       = "A. Hirschowitz and M. Maggesi",
 year         = "2012",
 title        = "Nested Abstract Syntax in Coq",
 journal      = "J. Autom. Reasoning",
 volume       = "49",
 number       = "3",
 pages        = "409--426",
 url          = "http://dx.doi.org/10.1007/s10817-010-9207-9",
)
@inproceedings(Hofmann:1999:SAH:788021.788940,
 author       = "M. Hofmann",
 year         = "1999",
 title        = "Semantical Analysis of Higher-Order Abstract Syntax",
 booktitle    = "Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science",
 series       = "LICS '99",
 publisher    = "IEEE Computer Society",
 address      = "Washington, DC, USA",
 pages        = "204--",
 url          = "http://dl.acm.org/citation.cfm?id=788021.788940",
)
@inproceedings(DBLP:conf/icalp/HonsellMS01,
 author       = "F. Honsell and M. Miculan and I. Scagnetto",
 year         = "2001",
 title        = "An Axiomatic Approach to Metareasoning on Nominal Algebras in HOAS",
 editor       = "Fernando Orejas and Paul G. Spirakis and Jan van Leeuwen",
 booktitle    = "ICALP",
 series       = "Lecture Notes in Computer Science",
 volume       = "2076",
 publisher    = "Springer",
 pages        = "963--978",
 url          = "http://dx.doi.org/10.1007/3-540-48224-5_78",
)
@article(HMS-01,
 author       = "F. Honsell and M. Miculan and I. Scagnetto",
 year         = "2001",
 title        = "pi-calculus in (Co)inductive-type theory",
 journal      = "Theor. Comput. Sci.",
 volume       = "253",
 number       = "2",
 pages        = "239--285",
 url          = "http://dx.doi.org/10.1016/S0304-3975(00)00095-5",
)
@article(DBLP:journals/entcs/HonsellMS01,
 author       = "F. Honsell and M. Miculan and I. Scagnetto",
 year         = "2001",
 title        = "The Theory of Contexts for First Order and Higher Order Abstract Syntax",
 journal      = "Electr. Notes Theor. Comput. Sci.",
 volume       = "62",
 pages        = "116--135",
 url          = "http://dx.doi.org/10.1016/S1571-0661(04)00323-8",
)
@misc(leroy:coq,
 author       = "X. Leroy",
 title        = "A solution to the POPLmark Challenge",
)
@techreport(Leroy-POPLmark,
 author       = "X. Leroy",
 year         = "2007",
 title        = "A locally nameless solution to the {POPLmark} challenge",
 type         = "Research report",
 number       = "6098",
 institution  = "INRIA",
)
@phdthesis(mik:eltop,
 author       = "M. Miculan",
 year         = "1997",
 title        = "Encoding Logical Theories of Programs",
 school       = "Dipartimento di Informatica, Universit\`a di Pisa, Italy",
)
@inproceedings(DBLP:conf/icfp/MiculanSH05,
 author       = "M. Miculan and I. Scagnetto and F. Honsell",
 year         = "2005",
 title        = "Translating specifications from nominal logic to CIC with the theory of contexts",
 editor       = "Randy Pollack",
 booktitle    = "MERLIN",
 publisher    = "ACM",
 pages        = "41--49",
 url          = "http://doi.acm.org/10.1145/1088454.1088460",
)
@article(DBLP:journals/tocl/MillerT05,
 author       = "D. Miller and A. Tiu",
 year         = "2005",
 title        = "A proof theory for generic judgments",
 journal      = "ACM Trans. Comput. Log.",
 volume       = "6",
 number       = "4",
 pages        = "749--783",
 url          = "http://doi.acm.org/10.1145/1094622.1094628",
)
@inproceedings(DBLP:conf/tlca/Paulin-Mohring93,
 author       = "C. Paulin-Mohring",
 year         = "1993",
 title        = "Inductive Definitions in the system Coq - Rules and Properties",
 editor       = "Marc Bezem and Jan Friso Groote",
 booktitle    = "TLCA",
 series       = "Lecture Notes in Computer Science",
 volume       = "664",
 publisher    = "Springer",
 pages        = "328--345",
 url          = "http://dx.doi.org/10.1007/BFb0037116",
)
@inproceedings(DBLP:conf/pldi/PfenningE88,
 author       = "F. Pfenning and C. Elliott",
 year         = "1988",
 title        = "Higher-Order Abstract Syntax",
 editor       = "Richard L. Wexelblat",
 booktitle    = "PLDI",
 publisher    = "ACM",
 pages        = "199--208",
 url          = "http://doi.acm.org/10.1145/53990.54010",
)
@book(DBLP:books/daglib/0005958,
 author       = "B. C. Pierce",
 year         = "2002",
 title        = "Types and programming languages",
 publisher    = "MIT Press",
)
@article(DBLP:journals/iandc/Pitts03,
 author       = "A. M. Pitts",
 year         = "2003",
 title        = "Nominal logic, a first order theory of names and binding",
 journal      = "Inf. Comput.",
 volume       = "186",
 number       = "2",
 pages        = "165--193",
 url          = "http://dx.doi.org/10.1016/S0890-5401(03)00138-X",
)
@misc(ricciotti:matita,
 author       = "W. Ricciotti",
 title        = "A solution to the POPLmark Challenge",
)
@article(DBLP:journals/entcs/ScagnettoM02,
 author       = "I. Scagnetto and M. Miculan",
 year         = "2002",
 title        = "Ambient Calculus and its Logic in the Calculus of Inductive Constructions",
 journal      = "Electr. Notes Theor. Comput. Sci.",
 volume       = "70",
 number       = "2",
 pages        = "76--95",
 url          = "http://dx.doi.org/10.1016/S1571-0661(04)80507-3",
)
@misc(stump:coq,
 author       = "A. Stump",
 title        = "A solution to the POPLmark Challenge",
)
@manual(coq,
 author       = "The Coq Development Team",
 year         = "2011",
 title        = "The Coq Proof Assitant Reference Manual, version 8.3",
 organization = "INRIA",
 url          = "http://coq.inria.fr/",
)
@misc(urban:isabelle,
 author       = "C. Urban\ et al.",
 title        = "A solution to the POPLmark Challenge",
)
@misc(xi:ats,
 author       = "H. Xi",
 title        = "A solution to the POPLmark Challenge",
)