@inproceedings(SASyLF,
 author       = {Jonathan Aldrich and Robert J. Simmons and Key Shin},
 year         = {2008},
 title        = {{SASyLF}: An Educational Proof Assistant for Language Theory},
 booktitle    = {International Workshop on Functional and Declarative Programming in Education},
 publisher    = {ACM Press},
 pages        = {31--40},
 doi          = {10.1145/1411260.1411266},
)
@inproceedings(Aydemir05TPHOLS,
 author       = {Brian E. Aydemir and Aaron Bohannon and Matthew Fairbairn and J. Nathan Foster and Benjamin C. Pierce and Peter Sewell and Dimitrios Vytiniotis and Geoffrey Washburn and Stephanie Weirich and Steve Zdancewic},
 year         = {2005},
 title        = {Mechanized Metatheory for the Masses: The {\textsc{PoplMark}} Challenge},
 booktitle    = {Eighteenth International Conference on Theorem Proving in Higher Order Logics},
 series       = {LNCS},
 volume       = {3603},
 publisher    = {Springer},
 pages        = {50--65},
 doi          = {10.1007/11541868\_4},
)
@inproceedings(THF0,
 author       = {Christoph Benzm{\"u}ller and Florian Rabe and Geoff Sutcliffe},
 year         = {2008},
 title        = {{THF0}---The Core of the {TPTP} Language for Higher-Order Logic},
 booktitle    = {Fourth International Joint Conference on Automated Reasoning},
 series       = {LNCS},
 volume       = {5195},
 publisher    = {Springer},
 pages        = {491--506},
 doi          = {10.1007/978-3-540-71070-7\_41},
)
@inproceedings(Cave:POPL12,
 author       = {Andrew Cave and Brigitte Pientka},
 year         = {2012},
 title        = {Programming with Binders and Indexed Data-Types},
 booktitle    = {Thirty-Ninth Annual {ACM} {SIGPLAN}-{SIGACT} Symposium on Principles of Programming Languages},
 publisher    = {ACM Press},
 pages        = {413--424},
 doi          = {10.1145/2103656.2103705},
)
@book(PLTbook,
 author       = {Matthias Felleisen and Robert Bruce Findler and Matthew Flatt},
 year         = {2009},
 title        = {Semantics Engineering with PLT Redex},
 publisher    = {The MIT Press},
)
@article(FeltyMomigliano:JAR10,
 author       = {Amy P. Felty and Alberto Momigliano},
 year         = {2012},
 title        = {Hybrid: A Definitional Two-Level Approach to Reasoning with Higher-Order Abstract Syntax},
 journal      = {Journal of Automated Reasoning},
 volume       = {48},
 number       = {1},
 pages        = {43--105},
 doi          = {10.1007/s10817-010-9194-x},
)
@article(orbi,
 author       = {Amy P. Felty and Alberto Momigliano and Brigitte Pientka},
 year         = {2015},
 title        = {The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations: Part 1---A Common Infrastructure for Benchmarks},
 journal      = {CoRR},
 volume       = {abs/1503.06095},
 url          = {http://arxiv.org/abs/1503.06095},
)
@article(companion,
 author       = {Amy P. Felty and Alberto Momigliano and Brigitte Pientka},
 year         = {2015},
 title        = {The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations: Part 2---A Survey},
 journal      = {Journal of Automated Reasoning},
 note         = {(to appear)},
)
@inproceedings(why3,
 author       = {Jean-Christophe Filli{\^a}tre},
 year         = {2013},
 title        = {One Logic To Use Them All},
 booktitle    = {Twenty-Fourth International Conference on Automated Deduction},
 series       = {LNCS},
 volume       = {7898},
 publisher    = {Springer},
 pages        = {1--20},
 doi          = {10.1007/978-3-642-38574-2\_1},
)
@inproceedings(Gacek:IJCAR08,
 author       = {Andrew Gacek},
 year         = {2008},
 title        = {The {A}bella Interactive Theorem Prover (System Description)},
 booktitle    = {Fourth International Joint Conference on Automated Reasoning},
 series       = {LNCS},
 volume       = {5195},
 publisher    = {Springer},
 pages        = {154--161},
 doi          = {10.1007/978-3-540-71070-7\_13},
)
@article(GacekMillerNadathur:JAR12,
 author       = {Andrew Gacek and Dale Miller and Gopalan Nadathur},
 year         = {2012},
 title        = {A Two-Level Logic Approach to Reasoning About Computations},
 journal      = {Journal of Automated Reasoning},
 volume       = {49},
 number       = {2},
 pages        = {241--273},
 doi          = {10.1007/s10817-011-9218-1},
)
@book(GirardLafontTaylor:proofsAndTypes,
 author       = {J.-Y. Girard and Y. Lafont and P. Tayor},
 year         = {1990},
 title        = {Proofs and Types},
 publisher    = {Cambridge University Press},
)
@inproceedings(HabliFelty:PXTP13,
 author       = {Nada Habli and Amy P. Felty},
 year         = {2013},
 title        = {Translating Higher-Order Specifications to {Coq} Libraries Supporting {Hybrid} Proofs},
 booktitle    = {Third International Workshop on Proof Exchange for Theorem Proving},
 series       = {EasyChair Proceedings in Computing},
 volume       = {14},
 pages        = {67--76},
)
@inproceedings(SATLIB,
 author       = {Holger H. Hoos and Thomas St{\"u}tzle},
 year         = {2000},
 title        = {SATLIB: An Online Resource for Research on {SAT}},
 booktitle    = {SAT 2000: Highlights of Satisfiability Research in the Year 2000},
 series       = {Frontiers in Artificial Intelligence and Applications},
 volume       = {63},
 publisher    = {IOS Press},
 pages        = {283--292},
)
@inproceedings(MMF07,
 author       = {Alberto Momigliano and Alan J. Martin and Amy P. Felty},
 year         = {2008},
 title        = {Two-Level {H}ybrid: A System for Reasoning Using Higher-Order Abstract Syntax},
 booktitle    = {Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2007},
 series       = {ENTCS},
 volume       = {196},
 publisher    = {Elsevier},
 pages        = {85--93},
 doi          = {10.1016/j.entcs.2007.09.019},
)
@inproceedings(Pientka07,
 author       = {Brigitte Pientka},
 year         = {2007},
 title        = {Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework {LF}},
 booktitle    = {Twentieth International Conference on Theorem Proving in Higher-Order Logics},
 series       = {LNCS},
 publisher    = {Springer},
 pages        = {246--261},
 doi          = {10.1007/978-3-540-74591-4\_19},
)
@inproceedings(Pientka:CADE15,
 author       = {Brigitte Pientka and Andrew Cave},
 year         = {2015},
 title        = {Inductive Beluga:Programming Proofs (System Description)},
 booktitle    = {Twenty-Fifth International Conference on Automated Deduction},
 publisher    = {Springer},
)
@inproceedings(Pientka:IJCAR10,
 author       = {Brigitte Pientka and Joshua Dunfield},
 year         = {2010},
 title        = {Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)},
 booktitle    = {Fifth International Joint Conference on Automated Reasoning},
 series       = {LNCS},
 volume       = {6173},
 publisher    = {Springer},
 pages        = {15--21},
 doi          = {10.1007/978-3-642-14203-1\_2},
)
@book(PierceFirstBook,
 author       = {Benjamin C. Pierce},
 year         = {2002},
 title        = {Types and Programming Languages},
 publisher    = {MIT Press},
)
@inproceedings(Schuermann:LFMTP08,
 author       = {Adam Poswolsky and Carsten Sch{\"{u}}rmann},
 year         = {2009},
 title        = {System Description: Delphin---{A} Functional Programming Language for Deductive Systems},
 booktitle    = {Third International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2008)},
 series       = {ENTCS},
 volume       = {228},
 publisher    = {Elsevier},
 pages        = {113--120},
 doi          = {10.1016/j.entcs.2008.12.120},
)
@inproceedings(RabeS09,
 author       = {Florian Rabe and Carsten Sch{\"{u}}rmann},
 year         = {2009},
 title        = {A Practical Module System for {LF}},
 booktitle    = {Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice},
 publisher    = {ACM Press},
 pages        = {40--48},
 doi          = {10.1145/1577824.1577831},
)
@article(RosuK,
 author       = {Ro{\c s}u, Grigore and {\c S}erb{\u a}nu{\c t}{\u a}, Traian Florin},
 year         = {2010},
 title        = {An Overview of the {K} Semantic Framework},
 journal      = {Journal of Logic and Algebraic Programming},
 volume       = {79},
 number       = {6},
 pages        = {397--434},
 doi          = {10.1016/j.jlap.2010.03.012},
)
@inproceedings(TwelfSP,
 author       = {Carsten Sch{\"u}rmann},
 year         = {2009},
 title        = {The {Twelf} Proof Assistant},
 booktitle    = {Twenty-Second International Conference on Theorem Proving in Higher Order Logics},
 series       = {LNCS},
 volume       = {5674},
 publisher    = {Springer},
 pages        = {79--83},
 doi          = {10.1007/978-3-642-03359-9\_7},
)
@article(ott,
 author       = {Peter Sewell and Francesco Zappa Nardelli and Scott Owens and Gilles Peskine and Thomas Ridge and Susmit Sarkar and Strni\v{s}a, Rok},
 year         = {2010},
 title        = {Ott: Effective Tool Support for the Working Semanticist},
 journal      = {Journal of Functional Programming},
 volume       = {20},
 number       = {1},
 pages        = {71--122},
 doi          = {10.1017/S0956796809990293},
)
@article(TPTP,
 author       = {Geoff Sutcliffe},
 year         = {2009},
 title        = {The {TPTP} Problem Library and Associated Infrastructure},
 journal      = {Journal of Automated Reasoning},
 volume       = {43},
 number       = {4},
 pages        = {337--362},
 doi          = {10.1007/s10817-009-9143-8},
)
@inproceedings(hoabella,
 author       = {Yuting Wang and Kaustuv Chaudhuri and Andrew Gacek and Gopalan Nadathur},
 year         = {2013},
 title        = {Reasoning About Higher-Order Relational Specifications},
 booktitle    = {Fifteenth International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming},
 publisher    = {ACM Press},
 pages        = {157--168},
 doi          = {10.1145/2505879.2505889},
)