@inproceedings(Altenkirch:TLCA93,
 author       = {Thorsten Altenkirch},
 year         = {1993},
 title        = {A Formalization of the Strong Normalization Proof for {System F} in {LEGO}},
 editor       = {Marc Bezem and Jan Friso Groote},
 booktitle    = {International Conference on Typed Lambda Calculi and Applications (TLCA '93)},
 series       = {Lecture Notes in Computer Science},
 volume       = {664},
 publisher    = {Springer},
 pages        = {13--28},
 doi          = {10.1007/BFb0037095},
)
@inproceedings(Berardi:WLF90,
 author       = {Stefano Berardi},
 year         = {1990},
 title        = {Girard Normalization Proof in {LEGO}},
 booktitle    = {Proceedings of the First Workshop on Logical Frameworks},
 pages        = {67--78},
)
@inproceedings(Cave:POPL12,
 author       = {Andrew Cave and Brigitte Pientka},
 year         = {2012},
 title        = {Programming with binders and indexed data-types},
 booktitle    = {{39th Annual {ACM} SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'12)}},
 publisher    = {ACM Press},
 pages        = {413--424},
 doi          = {10.1145/2103656.2103705},
)
@inproceedings(Cave:LFMTP13,
 author       = {Andrew Cave and Brigitte Pientka},
 year         = {2013},
 title        = {First-class substitutions in contextual type theory},
 booktitle    = {Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'13)},
 publisher    = {ACM Press},
 pages        = {15--24},
 doi          = {10.1145/2503887.2503889},
)
@incollection(CCoquand:92,
 author       = {Catarina Coquand},
 year         = {1992},
 title        = {A proof of normalization for simply typed lambda calculus writting in {ALF}},
 booktitle    = {Informal Proceedings of Workshop on Types for Proofs and Programs},
 publisher    = {Dept.\ of Computing Science, Chalmers Univ.\ of Technology and G{\"o}teborg Univ.},
 pages        = {80--87},
)
@incollection(Crary:ATAPL,
 author       = {Karl Crary},
 year         = {2005},
 title        = {Logical Relations and a Case Study in Equivalence Checking},
 editor       = {Bejamin C. Pierce},
 booktitle    = {Advanced Topics in Types and Programming Languages},
 publisher    = {The MIT Press},
)
@inproceedings(Doczkal:LFMTP09,
 author       = {Christian Doczkal and Jan Schwinghammer},
 year         = {2009},
 title        = {Formalizing a Strong Normalization Proof for {M}oggi's Computational Metalanguage: A Case Study in {Isabelle/HOL}-nominal},
 booktitle    = {Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'09)},
 publisher    = {ACM},
 pages        = {57--63},
 doi          = {10.1145/1577824.1577834},
)
@article(Momigliano:LFMTP07,
 author       = {Amy Felty and Alberto Momigliano},
 year         = {2012},
 title        = {Hybrid - {A} Definitional Two-Level Approach to Reasoning with Higher-Order Abstract Syntax},
 journal      = {J. Autom. Reasoning},
 volume       = {48},
 number       = {1},
 pages        = {43--105},
 doi          = {10.1007/s10817-010-9194-x},
)
@inproceedings(Gacek:IJCAR08,
 author       = {Andrew Gacek},
 year         = {2008},
 title        = {The {A}bella Interactive Theorem Prover (System Description)},
 booktitle    = {4th International Joint Conference on Automated Reasoning},
 series       = {Lecture Notes in Artificial Intelligence},
 volume       = {5195},
 publisher    = {Springer},
 pages        = {154--161},
 doi          = {10.1007/978-3-540-71070-7\_13},
)
@inproceedings(Gacek:LICS08,
 author       = {Andrew Gacek and Dale Miller and Gopalan Nadathur},
 year         = {2008},
 title        = {Combining generic judgments with recursive definitions},
 editor       = {F. Pfenning},
 booktitle    = {23rd Symposium on Logic in Computer Science},
 publisher    = {IEEE Computer Society Press},
 pages        = {33--44},
 doi          = {10.1109/LICS.2008.33},
)
@inproceedings(Gacek:LFMTP09,
 author       = {Andrew Gacek and Dale Miller and Gopalan Nadathur},
 year         = {2009},
 title        = {Reasoning in {A}bella about Structural Operational Semantics Specifications},
 booktitle    = {Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice (LFMTP 2008)},
 series       = {Electronic Notes in Theoretical Computer Science (ENTCS)},
 volume       = {228},
 publisher    = {Elsevier},
 pages        = {85 -- 100},
 doi          = {10.1016/j.entcs.2008.12.118},
)
@book(GirardLafontTaylor:proofsAndTypes,
 author       = {J.-Y. Girard and Y. Lafont and P. Tayor},
 year         = {1990},
 title        = {Proofs and types},
 publisher    = {Cambridge University Press},
)
@article(Harper93jacm,
 author       = {Robert Harper and Furio Honsell and Gordon Plotkin},
 year         = {1993},
 title        = {A Framework for Defining Logics},
 journal      = {{Journal of the ACM}},
 volume       = {40},
 number       = {1},
 pages        = {143--184},
 doi          = {10.1145/138027.138060},
)
@article(Harper03tocl,
 author       = {Robert Harper and Frank Pfenning},
 year         = {2005},
 title        = {On Equivalence and Canonical Forms in the {LF} Type Theory},
 journal      = {ACM Transactions on Computational Logic},
 volume       = {6},
 number       = {1},
 pages        = {61--101},
 doi          = {10.1145/1042038.1042041},
)
@article(Nanevski:ICML05,
 author       = {Aleksandar Nanevski and Frank Pfenning and Brigitte Pientka},
 year         = {2008},
 title        = {Contextual modal type theory},
 journal      = {{ACM Transactions on Computational Logic}},
 volume       = {9},
 number       = {3},
 pages        = {1--49},
 doi          = {10.1145/1352582.1352591},
)
@article(Narboux:LFMTP08,
 author       = {Julien Narboux and Christian Urban},
 year         = {2008},
 title        = {Formalising in {N}ominal {I}sabelle {C}rary's Completeness Proof for Equivalence Checking},
 journal      = {Electr. Notes Theor. Comput. Sci.},
 volume       = {196},
 pages        = {3--18},
 doi          = {10.1016/j.entcs.2007.09.014},
)
@inproceedings(Pfenning99cade,
 author       = {Frank Pfenning and Carsten Sch{\"u}rmann},
 year         = {1999},
 title        = {System Description: {Twelf} --- A Meta-Logical Framework for Deductive Systems},
 editor       = {H. Ganzinger},
 booktitle    = {{16th International Conference on Automated Deduction (CADE-16)}},
 series       = {Lecture Notes in Artificial Intelligence (LNAI 1632)},
 publisher    = {Springer},
 pages        = {202--206},
 doi          = {10.1007/3-540-48660-7\_14},
)
@inproceedings(Pientka:POPL08,
 author       = {Brigitte Pientka},
 year         = {2008},
 title        = {A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions},
 booktitle    = {{35th Annual {ACM} SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'08)}},
 publisher    = {ACM Press},
 pages        = {371--382},
 doi          = {10.1145/1328438.1328483},
)
@inproceedings(Pientka:TLCA15,
 author       = {Brigitte Pientka and Andreas Abel},
 year         = {2015},
 title        = {Structural Recursion over Contextual Objects},
 editor       = {Thorsten Altenkirch},
 booktitle    = {13th International Conference on Typed Lambda Calculi and Applications (TLCA'15)},
 publisher    = {Leibniz International Proceedings in Informatics (LIPIcs) of Schloss Dagstuhl},
 pages        = {273--287},
 doi          = {10.4230/LIPIcs.TLCA.2015.273},
)
@inproceedings(Pientka:CADE15,
 author       = {Brigitte Pientka and Andrew Cave},
 year         = {2015},
 title        = {Inductive Beluga:Programming Proofs (System description)},
 booktitle    = {25th International Conference on Automated Deduction (CADE-25)},
 publisher    = {Springer},
)
@inproceedings(Pientka:PPDP08,
 author       = {Brigitte Pientka and Joshua Dunfield},
 year         = {2008},
 title        = {Programming with proofs and explicit contexts},
 booktitle    = {{ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP'08)}},
 publisher    = {ACM Press},
 pages        = {163--173},
 doi          = {10.1145/1389449.1389469},
)
@inproceedings(Pientka:IJCAR10,
 author       = {Brigitte Pientka and Joshua Dunfield},
 year         = {2010},
 title        = {Beluga: a Framework for Programming and Reasoning with Deductive Systems ({System Description})},
 editor       = {J{\"u}rgen Giesl and Reiner Haehnle},
 booktitle    = {{5th International Joint Conference on Automated Reasoning (IJCAR'10)}},
 series       = {Lecture Notes in Artificial Intelligence (LNAI 6173)},
 publisher    = {Springer-Verlag},
 pages        = {15--21},
 doi          = {10.1007/978-3-642-14203-1\_2},
)
@inproceedings(Schuermann:ESOP08,
 author       = {Adam B. Poswolsky and Carsten Sch{\"u}rmann},
 year         = {2008},
 title        = {Practical programming with higher-order encodings and dependent types},
 booktitle    = {{17th European Symposium on Programming (ESOP '08)}},
 volume       = {4960},
 publisher    = {Springer},
 pages        = {93--107},
 doi          = {10.1007/978-3-540-78739-6\_7},
)
@inproceedings(Rasmussen:LFMTP13,
 author       = {Ulrik Rasmussen and Andrzej Filinski},
 year         = {2013},
 title        = {Structural Logical Relations with Case Analysis and Equality Reasoning},
 booktitle    = {Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP'13)},
 publisher    = {ACM Press},
 pages        = {43--54},
 doi          = {10.1145/2503887.2503891},
)
@inproceedings(Schurmann:LICS08,
 author       = {Carsten Sch{\"u}rmann and Jeffrey Sarnat},
 year         = {2008},
 title        = {Structural Logical Relations},
 booktitle    = {23rd Annual Symposium on Logic in Computer Science (LICS), Pittsburgh, PA, USA},
 publisher    = {IEEE Computer Society},
 pages        = {69--80},
 doi          = {10.1109/LICS.2008.44},
)
@article(Tait67,
 author       = {William Tait},
 year         = {1967},
 title        = {Intensional {I}nterpretations of {F}unctionals of {F}inite {T}ype {I}},
 journal      = {J. Symb. Log.},
 volume       = {32},
 number       = {2},
 pages        = {198--212},
 doi          = {10.2307/2271658},
)
@article(Urban:TOCL11,
 author       = {Christian Urban and James Cheney and Stefan Berghofer},
 year         = {2011},
 title        = {Mechanizing the metatheory of {LF}},
 journal      = {ACM Trans. Comput. Log.},
 volume       = {12},
 number       = {2},
 pages        = {15},
 doi          = {10.1145/1877714.1877721},
)