@string{lncs = {LNCS}}

@string{entcs = {ENTCS}}

@inproceedings{AltenkirchK16,
  author    = {Thorsten Altenkirch and
               Ambrus Kaposi},
  title     = {Type theory in type theory using quotient inductive types},
  booktitle = {{POPL}},
  pages     = {18--29},
  publisher = {{ACM}},
  year      = {2016}
}


@Article{Harper03tocl,
  author =       {Robert Harper and Frank Pfenning},
  title =        {On Equivalence and Canonical Forms in the {LF} Type Theory},
  journal =      {ACM Transactions on Computational Logic},
  volume    = {6},
  number    = {1},
  year      = {2005},
  pages     = {61-101},
}

@incollection{Crary:ATAPL,
 author = {Karl Crary},
 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},
 year = 2005
}

@article{Rabe:2013,
 author = {Rabe, Florian and Sojakova, Kristina},
 title = {Logical Relations for a Logical Framework},
 journal = {ACM Trans. Comput. Logic},
 issue_date = {November 2013},
 volume = {14},
 number = {4},
 month = nov,
 year = {2013},
 pages = {32:1--32:34},
 articleno = {32},
 numpages = {34},
 doi = {10.1145/2536740.2536741},
 acmid = {2536741},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {LF, Logical relation, Twelf, dependent type theory, logical framework, module system, parametricity},
} 



@inproceedings{AbelV14,
  author    = {Andreas Abel and
               Andrea Vezzosi},
  title     = {A Formalized Proof of Strong Normalization for Guarded Recursive Types},
  booktitle = {{APLAS}},
  series    = {Lecture Notes in Computer Science},
  volume    = {8858},
  pages     = {140--158},
  publisher = {Springer},
  year      = {2014}
}

@article{NarbouxU08,
  author    = {Julien Narboux and
               Christian Urban},
  title     = {Formalising in Nominal Isabelle Crary's Completeness Proof for Equivalence
               Checking},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {196},
  pages     = {3--18},
  year      = {2008}
}


@article{SORENSEN199735,
title = "Strong Normalization from Weak Normalization in Typed $\lambda$-Calculi",
journal = "Information and Computation",
volume = "133",
number = "1",
pages = "35 - 71",
year = "1997",
note = "",
issn = "0890-5401",
doi = "http://dx.doi.org/10.1006/inco.1996.2622",
url = "http://www.sciencedirect.com/science/article/pii/S089054019692622X",
author = "Morten Heine Sorensen",

}
@article{ABEL20083,
title = "Normalization for the Simply-Typed Lambda-Calculus in Twelf",
journal = "Electronic Notes in Theoretical Computer Science",
volume = "199",
number = "",
pages = "3 - 16",
year = "2008",
note = "Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages (LFM 2004)",
issn = "1571-0661",
doi = "http://dx.doi.org/10.1016/j.entcs.2007.11.009",
author = "Andreas Abel",
keywords = "Edinburgh Logical Framework",
keywords = "HOAS",
keywords = "Mechanized Proof",
keywords = "Normalization",
keywords = "Twelf"
}

@Article{Joachimski2003,
author="Joachimski, Felix
and Matthes, Ralph",
title="Short proofs of normalization for the simply- typed $\lambda$-calculus, permutative conversions and {G}{\"o}del's {T}",
journal="Archive for Mathematical Logic",
year="2003",
month="Jan",
day="01",
volume="42",
number="1",
pages="59--87",
abstract="{\enspace}Inductive characterizations of the sets of terms, the subset of strongly normalizing terms and normal forms are studied in order to reprove weak and strong normalization for the simply-typed $\lambda$-calculus and for an extension by sum types with permutative conversions. The analogous treatment of a new system with generalized applications inspired by generalized elimination rules in natural deduction, advocated by von Plato, shows the flexibility of the approach which does not use the strong computability/candidate style {\`a} la Tait and Girard. It is also shown that the extension of the system with permutative conversions by $\eta$-rules is still strongly normalizing, and likewise for an extension of the system of generalized applications by a rule of ``immediate simplification''. By introducing an infinitely branching inductive rule the method even extends to G{\"o}del's T.",
issn="1432-0665",
url="http://dx.doi.org/10.1007/s00153-002-0156-9"
}


@book{girardLafontTaylor,
author= {Girard, J.-Y. and Lafont, Y. and Tayor, P.},
title = {Proofs and types},
publisher = "Cambridge University Press",
year = {1990}
}
@inproceedings{BowmanA15,
  author    = {William J. Bowman and
               Amal Ahmed},
  title     = {Noninterference for free},
  booktitle = {{ICFP}},
  pages     = {101--113},
  publisher = {{ACM}},
  year      = {2015}
} 
@inproceedings{Ahmed15,
  author    = {Amal Ahmed},
  title     = {Verified Compilers for a Multi-Language World},
  booktitle = {{SNAPL}},
  series    = {LIPIcs},
  volume    = {32},
  pages     = {15--31},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  year      = {2015}
}
@inproceedings{NeisHKMDV15,
  author    = {Georg Neis and
               Chung{-}Kil Hur and
               Jan{-}Oliver Kaiser and
               Craig McLaughlin and
               Derek Dreyer and
               Viktor Vafeiadis},
  title     = {Pilsner: a compositionally verified compiler for a higher-order imperative
               language},
  booktitle = {{ICFP}},
  pages     = {166--178},
  publisher = {{ACM}},
  year      = {2015}
}
@inproceedings{Perconti14,
  author    = {James T. Perconti and
               Amal Ahmed},
  editor    = {Zhong Shao},
  title     = {Verifying an Open Compiler Using Multi-language Semantics},
  booktitle = {23rd European Symposium on Programming Languages and Systems {ESOP}},
  pages     = {128--148},
  series    = {Lecture Notes in Computer Science (LNCS 8410)},
  publisher = {Springer},
  year      = {2014},
  doi       = {10.1007/978-3-642-54833-8\_8}
}


@InProceedings{DeBruijn91lf,
  author = 	"N.G. de Bruijn",
  title = 	"A Plea for Weaker Frameworks",
  editor =	"G. Huet and G. Plotkin",
  pages =	"40--67",
  booktitle =	"Logical Frameworks",
  year =	1991,
  publisher =	"Cambridge University Press",
  keywords = 	"Automath"
}

@article{Statman85,
  author    = {Richard Statman},
  title     = {Logical Relations and the Typed lambda-Calculus},
  journal   = {Information and Control},
  volume    = {65},
  number    = {2/3},
  pages     = {85--97},
  year      = {1985}
}

@InProceedings{Coquand91,
  author =	"Thierry Coquand",
  title =	"An Algorithm for Testing Conversion in Type Theory",
  booktitle =	"Logical Frameworks",
  editor =	"G\'{e}rard Huet and Gordon Plotkin",
  publisher =	"Cambridge University Press",
  pages =	"255--279",
  year =	"1991",
  keywords = 	"LF, ALF"
}

@inproceedings{BentonH10,
  author    = {Nick Benton and
               Chung{-}Kil Hur},
  title     = {Step-Indexing: The Good, the Bad and the Ugly},
  booktitle = {Modelling, Controlling and Reasoning About State},
  series    = {Dagstuhl Seminar Proceedings},
  volume    = {10351},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik, Germany},
  year      = {2010}
}


@inproceedings{Altenkirch93,
  author    = {Thorsten Altenkirch},
  title     = {A Formalization of the Strong Normalization Proof for System {F} in
               {LEGO}},
  booktitle = {{TLCA}},
  series    = {Lecture Notes in Computer Science},
  volume    = {664},
  pages     = {13--28},
  publisher = {Springer},
  year      = {1993}
}

@article{Urban2011,
 author = {Urban, Christian and Cheney, James and Berghofer, Stefan},
 title = {Mechanizing the Metatheory of LF},
 journal = {ACM Trans. Comput. Logic},
 issue_date = {January 2011},
 volume = {12},
 number = {2},
 month = jan,
 year = {2011},
 issn = {1529-3785},
 pages = {15:1--15:42},
 articleno = {15},
 numpages = {42},
 doi = {10.1145/1877714.1877721},
 acmid = {1877721},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Logical frameworks, Nominal Isabelle, theorem provers},
}

@inproceedings{PientkaC15,
  author    = {Brigitte Pientka and
               Andrew Cave},
  title     = {Inductive Beluga: Programming Proofs},
  booktitle = {{CADE}},
  series    = {Lecture Notes in Computer Science},
  volume    = {9195},
  pages     = {272--281},
  publisher = {Springer},
  year      = {2015}
}

@article{BaeldeCGMNTW14,
  author    = {David Baelde and
               Kaustuv Chaudhuri and
               Andrew Gacek and
               Dale Miller and
               Gopalan Nadathur and
               Alwen Tiu and
               Yuting Wang},
  title     = {Abella: {A} System for Reasoning about Relational Specifications},
  journal   = {J. Formalized Reasoning},
  volume    = {7},
  number    = {2},
  pages     = {1--89},
  year      = {2014}
}

@inproceedings{hoabella,
  author =	 {Yuting Wang and Kaustuv Chaudhuri and Andrew Gacek
                  and Gopalan Nadathur},
  title =	 {Reasoning About Higher-Order Relational
                  Specifications},
  booktitle =	 {Fifteenth International ACM SIGPLAN Symposium on Principles and
                  Practice of Declarative Programming},
  year =	 2013,
  pages =	 {157--168},
  publisher =    {ACM Press}
}
@inproceedings{Pientka07,
  author    = {Brigitte Pientka},
  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},
  year      = {2007},
  publisher = {Springer},
  series    = lncs,
  pages     = {246--261}
}

@article{FMP17,
	author = {Felty, A. and Momigliano, A. and Pientka, B.},
	title = {Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions},
	year = {2017},
	journal = {MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE},
	doi = {10.1017/S0960129517000093},	
}

@inproceedings{TIP,
  author = {Koen Claessen and
               Moa Johansson and
               Dan Ros{\'{e}}n and
               Nicholas Smallbone},
  editor = {Manfred Kerber and
               Jacques Carette and
               Cezary Kaliszyk and
               Florian Rabe and
               Volker Sorge},
  title = {{TIP:} Tons of Inductive Problems},
  booktitle = {Intelligent Computer Mathematics - International Conference, {CICM}
               2015, Washington, DC, USA, July 13-17, 2015, Proceedings},
  series = {Lecture Notes in Computer Science},
  volume = {9150},
  pages = {333--337},
  publisher = {Springer},
  year = {2015},
  url = {http://dx.doi.org/10.1007/978-3-319-20615-8_23},
  doi = {10.1007/978-3-319-20615-8_23},
  timestamp = {Tue, 23 Jun 2015 13:20:42 +0200},
  biburl = {http://dblp.uni-trier.de/rec/bib/conf/mkm/ClaessenJRS15},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{FeltyMP15,
  author    = {Amy P. Felty and
               Alberto Momigliano and
               Brigitte Pientka},
  title     = {An Open Challenge Problem Repository for Systems Supporting Binders},
  booktitle = {{LFMTP}},
  series    = {{EPTCS}},
  volume    = {185},
  pages     = {18--32},
  year      = {2015}
}

@proceedings{DBLP:journals/corr/CervesatoC15,
  editor = {Iliano Cervesato and
               Kaustuv Chaudhuri},
  title = {Proceedings of the Tenth International Workshop on
                  Logical Frameworks and Meta Languages: Theory and
                  Practice, {LFMTP} 2015, Berlin, Germany, August 1,
                  2015},
  series = {{EPTCS}},
  volume = {185},
  year = {2015},
  doi = {10.4204/EPTCS.185},
  timestamp = {Fri, 07 Aug 2015 13:54:18 +0200},
  biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/CervesatoC15},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{Wang:2013,
  author = {Wang, Yuting and Nadathur, Gopalan},
  title = {Towards Extracting Explicit Proofs from Totality Checking in {Twelf}},
  booktitle = {Eighth ACM SIGPLAN International Workshop on Logical
                  Frameworks and Meta-languages: Theory and Practice},
  year = 2013,
  publisher = {ACM Press},
  pages = {55--66}
}

@article{NOM-JAR,
  author = {Maribel Fern{\'a}ndez and
               Christian Urban},
  title = {Preface: Theory and Applications of Abstraction, Substitution
               and Naming},
  journal = {Journal of Automated Reasoning},
  volume = {49},
  number = {2},
  year = {2012},
  pages = {111--114}
}

@article{POPL-JAR,
  author = {Benjamin C. Pierce and
               Stephanie Weirich},
  title = {Preface to Special Issue: The {\textsc{PoplMark}} Challenge},
  journal = {Journal of Automated Reasoning},
  volume = {49},
  number = {3},
  year = {2012},
  pages = {301--302}
}

@article{companion,
  year = {2015},
  issn = {0168-7433},
  journal = {Journal of Automated Reasoning},
  doi = {10.1007/s10817-015-9327-3},
  title = {The Next 700 Challenge Problems for Reasoning with
                  Higher-Order Abstract Syntax Representations: Part
                  2---A Survey},
  publisher = {Springer Netherlands},
  keywords = {Logical frameworks; Higher-order abstract syntax; Proof assistants; Benchmarks; Context reasoning},
  author = {Felty, Amy and Momigliano, Alberto and Pientka, Brigitte},
  pages = {307--372},
  language = {English},
  volume = 55,
  number = 4
}

@article{DonnellyX07,
  author    = {Kevin Donnelly and
               Hongwei Xi},
  title     = {A Formalization of Strong Normalization for Simply-Typed Lambda-Calculus
               and System {F}},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {174},
  number    = {5},
  pages     = {109--125},
  year      = {2007}
}

@inproceedings{Cave:POPL12,
  author = {Andrew Cave and Brigitte Pientka},
  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},
  year = 2012
}

@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},
  title = {Mechanized Metatheory for the Masses: The {\textsc{PoplMark}}
                  Challenge},
  pages = {50--65},
  booktitle = {TPHOLs},
  series = lncs,
  volume = 3603,
  year = 2005,
  publisher = {Springer}
}

%  booktitle = {Eighteenth International Conference on Theorem Proving in
%                  Higher Order Logics},


@article{FeltyMomigliano:JAR10,
  author = {Amy P. Felty and Alberto Momigliano},
  title = {Hybrid: A Definitional Two-Level Approach to
                  Reasoning with Higher-Order Abstract Syntax},
  journal = {Journal of Automated Reasoning},
  volume = 48,
  number = 1,
  year = 2012,
  pages = {43-105}
}

@book{PierceFirstBook,
  author = {Benjamin C. Pierce},
  title = {Types and Programming Languages},
  publisher = {MIT Press},
  year = 2002,
  plclub = {Yes},
  bcp = {Yes},
  keys = {books},
  homepage = {http://www.cis.upenn.edu/~bcpierce/tapl},
  errata = {http://www.cis.upenn.edu/~bcpierce/tapl/errata.txt}
}

@article{GacekMillerNadathur:JAR12,
  author = {Andrew Gacek and Dale Miller and Gopalan Nadathur},
  title = {A Two-Level Logic Approach to Reasoning About
                  Computations},
  journal = {Journal of Automated Reasoning},
  volume = 49,
  number = 2,
  year = 2012,
  pages = {241--273}
}

@inproceedings{Gacek:IJCAR08,
  author = {Andrew Gacek},
  title = {The {A}bella Interactive Theorem Prover (System
                  Description)},
  year = 2008,
  booktitle = {Fourth International Joint Conference on Automated
                  Reasoning},
  pages = {154--161},
  publisher = {Springer},
  series = lncs,
  volume = 5195
}

@book{girardLafontTaylor:proofsAndTypes,
  author = {Girard, J.-Y. and Lafont, Y. and Tayor, P.},
  title = {Proofs and Types},
  publisher = {Cambridge University Press},
  year = 1990
}

@article{Harper93jacm,
  author = {Robert Harper and Furio Honsell and Gordon Plotkin},
  title = {A Framework for Defining Logics},
  journal = {Journal of the Association for Computing Machinery},
  year = 1993,
  volume = 40,
  number = 1,
  pages = {143--184},
  month = jan,
  keywords = {LF},
  urldvi = {http://www.cs.cmu.edu/~fp/elf-papers/jacm93.dvi.gz}
}

@article{HarperLicata:JFP07,
  author = {Robert Harper and Daniel R. Licata},
  title = {Mechanizing Metatheory in a Logical Framework},
  journal = {Journal of Functional Programming},
  year = 2007,
  volume = 17,
  number = {4-5},
  pages = {613--673},
  publisher = {Cambridge University Press}
}

@inproceedings{Howe,
  author = {Momigliano, Alberto},
  title = {A Supposedly Fun Thing {I} May Have to Do Again: A
                  {HOAS} Encoding of {Howe}'s Method},
  booktitle = {Seventh ACM SIGPLAN International Workshop on Logical
  	       	  Frameworks and Meta-Languages, Theory and Practice},
  publisher = {ACM Press},
  year = 2012,
  pages = {33--42}
}

@inproceedings{MMF07,
  author = {Alberto Momigliano and Alan J. Martin and Amy P. Felty},
  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 2008},
  series = entcs,
  volume = 196,
  year = 2008,
  pages = {85--93},
  publisher = {Elsevier}
}

@article{MartinLof85,
  author = {Per Martin-L{\"o}f},
  title = {On the Meanings of the Logical Constants and the
                  Justifications of the Logical Laws},
  journal = {Nordic Journal of Philosophical Logic},
  year = 1996,
  volume = 1,
  number = 1,
  pages = {11--60}
}

@article{Miller91jlc,
  author = {Dale Miller},
  title = {A Logic Programming Language with
                  Lambda-Abstraction, Function Variables, and Simple
                  Unification},
  journal = {Journal of Logic and Computation},
  year = 1991,
  volume = 1,
  number = 4,
  pages = {497--536},
  keywords = {lambda-Prolog, unification},
  urldvi = {file://ftp.cis.upenn.edu/pub/papers/miller/jlc91.dvi.Z}
}

@unpublished{Pfenning01book,
  author = {Frank Pfenning},
  title = {Computation and Deduction},
  note = {\url{http://www.cs.cmu.edu/~fp/courses/comp-ded/handouts/cd.pdf},
            Accessed 26 October 2016},
  year = 2001,
  keywords = {LF, Elf},
  url = {http://www.cs.cmu.edu/~fp/courses/comp-ded/handouts/cd.pdf},
  optannote = {}
}

@article{MillerP99,
  author = {Dale Miller and
               Catuscia Palamidessi},
  title = {Foundational Aspects of Syntax},
  journal = {ACM Computing Surveys},
  volume = {31},
  number = {3es},
  year = {1999},
  pages = {1--6},
  note = {{Article No. 11}},
  ee = {http://doi.acm.org/10.1145/333580.333590},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{Pientka:PPDP08,
  author = {Brigitte Pientka and Joshua Dunfield},
  title = {Programming with Proofs and Explicit Contexts},
  booktitle = {Tenth ACM SIGPLAN International Conference on
                  Principles and Practice of Declarative Programming},
  pages = {163--173},
  publisher = {ACM Press},
  year = 2008
}

@inproceedings{Pientka:CADE15,
  author = {Brigitte Pientka and Andrew Cave},
  title = {Inductive {B}eluga: Programming Proofs (System description)},
  editor = {Amy P. Felty and Aart Middeldorp},
  optcrossref = {},
  optkey = {},
  booktitle = {25th International Conference on Automated Deduction (CADE-25)},
  pages = {272--281},
  year = {2015},
  series = {Lecture Notes in Computer Science},
  volume = {9195},
  publisher = {Springer}
}

@inproceedings{Pientka:IJCAR10,
  author = {Brigitte Pientka and Joshua Dunfield},
  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,
  pages = {15--21},
  publisher = {Springer},
  year = 2010
}

@inproceedings{Pientka:POPL08,
  author = {Brigitte Pientka},
  title = {A Type-Theoretic Foundation for Programming with
                  Higher-Order Abstract Syntax and First-Class
                  Substitutions},
  booktitle = {Thirty-Fifth Annual {ACM} {SIGPLAN}-{SIGACT} Symposium on
                  Principles of Programming Languages},
  publisher = {ACM Press},
  pages = {371--382},
  year = 2008
}
@inproceedings{CaveP15,
  author    = {Andrew Cave and
               Brigitte Pientka},
  title     = {A Case Study on Logical Relations using Contextual Types},
  booktitle = {{LFMTP}},
  series    = {{EPTCS}},
  volume    = {185},
  pages     = {33--45},
  year      = {2015}
}

@inproceedings{Schuermann:ESOP08,
  author = {Adam B. Poswolsky and Carsten Sch{\"u}rmann},
  title = {Practical Programming with Higher-Order Encodings
                  and Dependent Types},
  booktitle = {Seventeenth European Symposium on Programming},
  pages = {93--107},
  year = 2008,
  series = lncs,
  volume = 4960,
  publisher = {Springer}
}

@phdthesis{Schurmann00phd,
  author = {Carsten Sch{\"u}rmann},
  title = {Automating the Meta Theory of Deductive Systems},
  school = {Department of Computer Science, Carnegie Mellon
                  University},
  year = 2000,
  month = aug,
  note = {Available as Technical Report CMU-CS-00-146}
}

@article{Appel:2001,
 author = {Appel, Andrew W. and McAllester, David},
 title = {An Indexed Model of Recursive Types for Foundational Proof-carrying Code},
 journal = {ACM Trans. Program. Lang. Syst.},
 issue_date = {September 2001},
 volume = {23},
 number = {5},
 month = sep,
 year = {2001},
 issn = {0164-0925},
 pages = {657--683},
 numpages = {27},
 doi = {10.1145/504709.504712},
 acmid = {504712},
 publisher = {ACM},
 address = {New York, NY, USA},
} 


@inproceedings{Schurmann:LICS08,
  author = {Carsten Sch{\"u}rmann and Jeffrey Sarnat},
  title = {Structural Logical Relations},
  booktitle = {Twenty-Third Annual IEEE Symposium on Logic in
                  Computer Science},
  year = 2008,
  publisher = {IEEE Computer Society},
  pages = {69--80}
}

@inproceedings{schurmann03tphols,
  author = {Carsten Sch{\"u}rmann and Frank Pfenning},
  title = {A Coverage Checking Algorithm for {LF}},
  booktitle = {Sixteenth International Conference on Theorem Proving in
                  Higher Order Logics},
  pages = {120--135},
  year = 2003,
  volume = 2758,
  series = lncs,
  publisher = {Springer}
}

@article{MomiglianoAC02,
  author    = {Alberto Momigliano and
               Simon Ambler and
               Roy L. Crole},
  title     = {A {H}ybrid Encoding of {H}owe's Method for Establishing Congruence of
               Bisimilarity},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {70},
  number    = {2},
  pages     = {60--75},
  year      = {2002}
}


@inproceedings{CSL,
  author = {Alberto Momigliano},
  title = {Elimination of Negation in a Logical Framework},
  booktitle = {Computer Sceince Logic},
  year = {2000},
  pages = {411--426},
  volume = 1862,
  series = lncs,
  publisher = {Springer}
}

@inproceedings{TwelfSP,
  author = {Carsten Sch{\"u}rmann},
  title = {The {Twelf} Proof Assistant},
  booktitle = {Twenty-Second International Conference on Theorem Proving in
                  Higher Order Logics},
  year = 2009,
  pages = {79--83},
  volume = 5674,
  series = lncs,
  publisher = {Springer}
}


@inproceedings{Crary09,
  author = {Karl Crary},
  title = {Explicit Contexts in {LF} (Extended Abstract)},
  booktitle = {Third International Workshop on
                  Logical Frameworks and Meta-Languages: Theory and
                  Practice, LFMTP 2008},
  series = entcs,
  volume = 228,
  year = 2009,
  pages = {53--68},
  publisher = {Elsevier}
}

@article{TPTP,
  author = {Geoff Sutcliffe},
  title = {The {TPTP} Problem Library and Associated
                  Infrastructure},
  journal = {Journal of Automated Reasoning},
  volume = 43,
  number = 4,
  year = 2009,
  pages = {337-362}
}

@inproceedings{SATLIB,
  author = {Holger H. Hoos and Thomas St{\"u}tzle},
  booktitle = {SAT 2000: Highlights of Satisfiability Research in the
                  Year 2000},
  editor = {I. Gent and H. Van Maaren and T. Walsh},
  pages = {283--292},
  publisher = {IOS Press},
  title = {SATLIB: An Online Resource for Research on {SAT}},
  series = {Frontiers in Artificial Intelligence and Applications},
  volume = 63,
  year = 2000
}

