@String{LNCS = {Lecture Notes in Computer Science}}

@InProceedings{TT-lifting,
    author = {Samuel Lindley and Ian Stark },
    title = {\href{https://doi.org/10.1007/11417170_20}{Reducibility and {$\top\top$}-lifting for Computation Types}},
    booktitle = {Proceedings of Typed Lambda Calculi and Applications ({TLCA '05})},
    publisher = {Springer},
    year = 2005,
    month = {Apr},
	series = lncs,
    volume = {3461},
    pages = {262-277},
    doi = {10.1007/11417170_20},
    url = {http://www.inf.ed.ac.uk/~stark/reducibility.html},
}


@book{proofs+types,
 author = {Girard,, Jean-Yves and Taylor,, Paul and Lafont,, Yves},
 title = {Proofs and Types},
 year = {1989},
 isbn = {0-521-37181-3},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
 }

@article{nominal-techniques,
 author = {Urban,, Christian},
 title = {\href{https://doi.org/10.1007/s10817-008-9097-2}{Nominal Techniques in {Isabelle/HOL}}},
 journal = {J. Autom. Reason.},
 volume = {40},
 number = {4},
 year = {2008},
 issn = {0168-7433},
 pages = {327--356},
 doi = {https://doi.org/10.1007/s10817-008-9097-2},
 publisher = {Kluwer Academic Publishers},
 address = {Hingham, MA, USA},
}


@article{FO-nominal,
 author = {Pitts,, Andrew M.},
 title = {\href{https://doi.org/10.1016/S0890-5401(03)00138-X}{Nominal logic, a first order theory of names and binding}},
 journal = {Inf. Comput.},
 volume = {186},
 number = {2},
 year = {2003},
 issn = {0890-5401},
 pages = {165--193},
 doi = {https://doi.org/10.1016/S0890-5401(03)00138-X},
 publisher = {Academic Press, Inc.},
 address = {Duluth, MN, USA},
 }

@article{alpha-structural,
 author = {Pitts,, Andrew M.},
 title = {\href{http://doi.acm.org/10.1145/1147954.1147961}{Alpha-structural recursion and induction}},
 journal = {J. ACM},
 volume = {53},
 number = {3},
 year = {2006},
 issn = {0004-5411},
 pages = {459--506},
 doi = {http://doi.acm.org/10.1145/1147954.1147961},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@InProceedings{FM-HOL,
  author = {Murdoch J. Gabbay},
  title = {{FM-HOL}, a higher-order theory of names},
  booktitle = {35 Years of Automath},
  year = {2002},
  editor = {F. Kamareddine},
  month = {April},
  organization = {Heriot-Watt University, Edinburgh, Scotland},
}

@book{isabelle-generic,
 author = {L. C. Paulson and T. Nipkow},
 title = {Isabelle: A Generic Theorem Prover},
 series= {Lecture Notes in Computer Science},
 publisher = {Springer Berlin / Heidelberg} ,
 issn = {0302-9743 (Print) 1611-3349 (Online)},
 volume = {828/1994},
 doi = {10.1007/BFb0030541},
 year = 1994
}

@phdthesis{isar-thesis,
  author = { Markus M. Wenzel },
  title = {Isabelle/Isar -- a versatile environment for human-readable formal proof documents},
  school = {Technische Universi\"at M\"unchen},
  year = {2002},
  note = {Revised version to cover Isabelle 2002}
}

@article{isabelle-foundation,
 author = {Paulson,, L. C.},
 title = {\href{https://doi.org/10.1007/BF00248324}{The foundation of a generic theorem prover}},
 journal = {J. Autom. Reason.},
 volume = {5},
 number = {3},
 year = {1989},
 issn = {0168-7433},
 pages = {363--397},
 doi = {https://doi.org/10.1007/BF00248324},
 publisher = {Kluwer Academic Publishers},
 address = {Hingham, MA, USA},
 }

@article{Huet75,
  author    = {G{\'e}rard P. Huet},
  title     = {A Unification Algorithm for Typed lambda-Calculus},
  journal   = {Theor. Comput. Sci.},
  volume    = {1},
  number    = {1},
  year      = {1975},
  pages     = {27-57},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@manual{isar-overview,
	author = {Tobias Nipkow},
	title = {A Tutorial Introduction to Structured Isar Proofs},
	url = {http://isabelle.in.tum.de/dist/Isabelle/doc/isar-overview.pdf},
	note = {\href{http://isabelle.in.tum.de/dist/Isabelle/doc/isar-overview.pdf}{http://isabelle.in.tum.de/dist/Isabelle/doc/isar-overview.pdf}}
}

@manual{isar-ref,
	author = {Makarius Wenzel},
	title = {The Isabelle/Isar Reference Manual},
	url = {http://isabelle.in.tum.de/dist/Isabelle/doc/isar-ref.pdf},
	note = {\href{http://isabelle.in.tum.de/dist/Isabelle/doc/isar-ref.pdf}{http://isabelle.in.tum.de/dist/Isabelle/doc/isar-ref.pdf}},
	month = {June},
	year = {2008}
}

@manual{isabelle-tutorial,
	author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
	title = {A Proof Assistant for Higher-Order Logic},
	month = {April},
	year = {2009},
	note = {\href{http://isabelle.in.tum.de/dist/Isabelle/doc/tutorial.pdf}{http://isabelle.in.tum.de/dist/Isabelle/doc/tutorial.pdf}},
	url = {http://isabelle.in.tum.de/dist/Isabelle/doc/tutorial.pdf},
}

@manual{isabelle-ref,
	author = {Lawrence C. Paulson and Tobias Nipkow and Markus Wenzel},
	title = {Old Isabelle Reference Manual},
	month = {April},
	year = {2009},
	note = {\href{http://isabelle.in.tum.de/dist/Isabelle/doc/ref.pdf}{http://isabelle.in.tum.de/dist/Isabelle/doc/ref.pdf}},
	url = {http://isabelle.in.tum.de/dist/Isabelle/doc/ref.pdf}
}

@inproceedings{structural-LR,
 author = {Sch\"{u}rmann,, Carsten and Sarnat,, Jeffrey},
 title = {\href{https://doi.org/10.1109/LICS.2008.44}{Structural Logical Relations}},
 booktitle = {LICS '08: Proceedings of the 2008 23rd Annual IEEE Symposium on Logic in Computer Science},
 year = {2008},
 isbn = {978-0-7695-3183-0},
 pages = {69--80},
 doi = {https://doi.org/10.1109/LICS.2008.44},
 publisher = {IEEE Computer Society},
 address = {Washington, DC, USA},
 }

 @INPROCEEDINGS{vc-compat,
    author = {Christian Urban and Stefan Berghofer and Michael Norrish},
    title = {Barendregt’s variable convention in rule inductions},
    booktitle = {CADE '07: Proceedings of the 21th International Conference on Automated Deduction},
	volume = {4603},
	series = LNCS,
    year = {2007},
    pages = {35--50},
    publisher = {Springer}
}

@inproceedings{engineering-metatheory,
 author = {Aydemir,, Brian and Chargu\'{e}raud,, Arthur and Pierce,, Benjamin C. and Pollack,, Randy and Weirich,, Stephanie},
 title = {\href{http://doi.acm.org/10.1145/1328438.1328443}{Engineering formal metatheory}},
 booktitle = {{POPL '08}: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
 year = {2008},
 isbn = {978-1-59593-689-9},
 pages = {3--15},
 location = {San Francisco, California, USA},
 doi = {http://doi.acm.org/10.1145/1328438.1328443},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@ARTICLE{bruijn-index,
    author = {N. G. De Bruijn},
    title = {Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser Theorem},
    journal = {Indag. Math},
    year = {1972},
    volume = {34},
    pages = {381--392}
}

@ARTICLE{somelambda,
    author = {James Mckinna and Robert Pollack},
    title = {Some lambda calculus and type theory formalized},
    journal = {J. Autom. Reason.},
    year = {1999},
    volume = {23},
    pages = {373-409}
}

@article{lnr-poplmark,
	location = {http://www.scientificcommons.org/20032191},
	title = {A locally nameless solution to the POPLmark challenge},
	author = {Leroy, Xavier},
	year = {2007},
	keywords = {Computer Science/Programming Languages, Computer Science/Logic in Computer Science, POPLmark, Coq, locally nameless, alpha-conversion, binders, type systems, metatheory, system F-sub},
	abstract = {The POPLmark challenge is a collective experiment intended to assess the usability of theorem provers and proof assistants in the context of fundamental research on programming languages. In this report, we present a solution to the challenge, developed with the Coq proof assistant, and using the "locally nameless" presentation of terms with binders introduced by McKinna, Pollack, Gordon, and McBride.},
	publisher = {HAL - CCSD},
	note = {\href{http://hal.inria.fr/inria-00123945/en/}{http://hal.inria.fr/inria-00123945/en/}},
	institution = {INRIA a CCSD electronic archive server based on P.A.O.L [http://hal.inria.fr/oai/oai.php] (France)},
}

@article{lambda-comp,
 author = {Moggi,, Eugenio},
 title = {\href{https://doi.org/10.1016/0890-5401(91)90052-4}{Notions of computation and monads}},
 journal = {Inf. Comput.},
 volume = {93},
 number = {1},
 year = {1991},
 issn = {0890-5401},
 pages = {55--92},
 doi = {https://doi.org/10.1016/0890-5401(91)90052-4},
 publisher = {Academic Press, Inc.},
 address = {Duluth, MN, USA},
 }

@article{coc,
 author = {Coquand,, Thierry and Huet,, Gerard},
 title = {\href{https://doi.org/10.1016/0890-5401(88)90005-3}{The calculus of constructions}},
 journal = {Inf. Comput.},
 volume = {76},
 number = {2-3},
 year = {1988},
 issn = {0890-5401},
 pages = {95--120},
 doi = {https://doi.org/10.1016/0890-5401(88)90005-3},
 publisher = {Academic Press, Inc.},
 address = {Duluth, MN, USA},
 }

@INPROCEEDINGS{cbpv-subsuming,
    author = {Paul Blain Levy},
    title = {Call-By-Push-Value: A Subsuming Paradigm},
    booktitle = {TLCA},
    year = {1999},
    pages = {228--242},
	series = lncs,
	volume = {1581},
    publisher = {Springer-Verlag}
}

@incollection{fm-models,
	author = {Thomas J. Jech},
	booktitle = {Lectures in Set Theory with Particular Emphasis on the Method of Forcing},
	title = {\href{https://doi.org/10.1007/BFb0061156}{Fraenkel-Mostowski models}},
	pages = {122-125},
	year = {1971},
	series = {Lecture Notes in Mathematics},
	volume = {217},
	doi = {https://doi.org/10.1007/BFb0061156},
	publisher = {Springer}
}

@misc{SN.thy,
	author = {{Nominal Methods Group}},
	title = {Strong Normalisation proof from the Proofs and Types book},
	note = {\href{http://isabelle.in.tum.de/dist/library/HOL/HOL-Nominal/Examples/SN.html}{http://isabelle.in.tum.de/dist/library/ HOL/HOL-Nominal/Examples/SN.html}}
}

@misc{poplmark,
	title = {Mechanized Metatheory for the Masses: The PoplMark Challenge},
	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 },
	note = {\href{http://www.cis.upenn.edu/~plclub/wiki-static/poplmark.pdf}{http://www.cis.upenn.edu/\textasciitilde plclub/ wiki-static/poplmark.pdf}},
	year = 2005
}

@article{benton-comp-log,
 author = {Benton,, P. N. and Bierman,, G. M. and De Paiva,, V. C. V.},
 title = {\href{https://doi.org/10.1017/S0956796898002998}{Computational types from a logical perspective}},
 journal = {J. Funct. Program.},
 volume = {8},
 number = {2},
 year = {1998},
 issn = {0956-7968},
 pages = {177--193},
 doi = {https://doi.org/10.1017/S0956796898002998},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
 }

@mastersthesis{BA-thesis,
	type = {{B.Sc.} thesis},
	author = {Christian Doczkal},
	title = {Strong Normalisation of Call-By-Push-Value},
	school = {Universit\"{a}t des Saarlandes},
	year = 2007
}

@BOOK{Baren1985,
   author={Barendregt, Hendrik Pieter},
   title={The lambda calculus},
   publisher={Elsevier/North-Holland},
   year={1985},
   volume={103},
   series={Studies in logic and the foundations of mathematics},
   edition={rev. ed., 2nd printing 1985}
}

@inproceedings{goguen,
 author = {Goguen,, Healfdene},
 title = {Typed Operational Semantics},
 booktitle = {TLCA '95: Proceedings of the Second International Conference on Typed Lambda Calculi and Applications},
 year = {1995},
 isbn = {3-540-59048-X},
 pages = {186--200},
 publisher = {Springer-Verlag},
 address = {London, UK},
 }

@article{domain-free,
 author = {Barthe,, Gilles and S\o{}rensen,, Morten Heine},
 title = {\href{https://doi.org/10.1017/S0956796800003750}{Domain-free pure type systems}},
 journal = {J. Funct. Program.},
 volume = {10},
 number = {5},
 year = {2000},
 issn = {0956-7968},
 pages = {417--452},
 doi = {https://doi.org/10.1017/S0956796800003750},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
 }

@inproceedings{Altenkirch:93,
  author    = {Thorsten Altenkirch},
  title     = {\href{https://doi.org/10.1007/BFb0037095}{A formalization of the strong normalization proof for {System
               F} in {LEGO}}},
  booktitle = {TLCA},
  year      = {1993},
  pages     = {13--28},
  publisher = {Springer-Verlag},
  series    = LNCS,
  volume    = {664},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{reynolds-SystemF,
 author = {Reynolds, John C.},
 title = {Towards a theory of type structure},
 booktitle = {Programming Symposium, Proceedings Colloque sur la Programmation},
 year = {1974},
 isbn = {3-540-06859-7},
 pages = {408--423},
 publisher = {Springer-Verlag},
 address = {London, UK},
 }


@article{koenig,
 author = {D{\'{e}}nes K{\H{o}}nig},
 title = {Sur les correspondances multivoques des ensembles},
 journal = {Fund. Math.},
 year = 1926,
 pages = {114-134},
 volume = 8,
}

@inproceedings{nominal-inversion,
 author = {Berghofer, Stefan and Urban, Christian},
 title = {\href{https://doi.org/10.1007/978-3-540-71067-7_10}{Nominal Inversion Principles}},
 series = LNCS,
 volume = {5170},
 booktitle = {TPHOLs '08: Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics},
 year = {2008},
 isbn = {978-3-540-71065-3},
 pages = {71--85},
 location = {Montreal, P.Q., Canada},
 doi = {https://doi.org/10.1007/978-3-540-71067-7_10},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
 }


@article{hhp93lf,
 author = {Robert Harper and Furio Honsell and Gordon Plotkin},
 title = {\href{http://doi.acm.org/10.1145/138027.138060}{A framework for defining logics}},
 journal = {J. ACM},
 volume = {40},
 number = {1},
 year = {1993},
 issn = {0004-5411},
 pages = {143--184},
 doi = {http://doi.acm.org/10.1145/138027.138060},
 publisher = {ACM Press},
 address = {New York, NY, USA},
 }


@inproceedings{sets-types,
 author = {Werner, Benjamin},
 title = {Sets in Types, Types in Sets},
 booktitle = {TACS '97: Proceedings of the Third International Symposium on Theoretical Aspects of Computer Software},
 year = {1997},
 isbn = {3-540-63388-X},
 pages = {530--346},
 publisher = {Springer-Verlag},
 address = {London, UK},
 }


@inproceedings{inductive-types,
 author = {Coquand, Thierry and Paulin, Christine},
 title = {Inductively defined types},
 booktitle = {COLOG '88: Proceedings of the International Conference on Computer Logic},
 year = {1990},
 isbn = {3-540-52335-9},
 pages = {50--66},
 publisher = {Springer-Verlag},
 address = {London, UK},
 }

@article{Berger:Berghofer:Letouzey:Schwichtenberg:06,
  author    = {Ulrich Berger and
               Stefan Berghofer and
               Pierre Letouzey and
               Helmut Schwichtenberg},
  title     = {\href{https://doi.org/10.1007/s11225-006-6604-5}{Program extraction from normalization proofs}},
  journal   = {Stud. Log.},
  volume    = {82},
  number    = {1},
  year      = {2006},
  pages     = {25--49},
  ee        = {https://doi.org/10.1007/s11225-006-6604-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{Donnelly:Xi:07,
  author    = {Kevin Donnelly and
               Hongwei Xi},
  title     = {\href{https://doi.org/10.1016/j.entcs.2007.01.021}{A formalization of strong normalization for simply-typed
               lambda-calculus and {System F}}},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {174},
  number    = {5},
  year      = {2007},
  pages     = {109--125},
  ee        = {https://doi.org/10.1016/j.entcs.2007.01.021},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@InProceedings{Abel:04,
  author    = {Andreas Abel},
  title     = {\href{http://www.tcs.informatik.uni-muenchen.de/~abel}{Normalization for the Simply Typed $\lambda$-calculus in {Twelf}}},
  booktitle = {{LFM'04}: Fourth International Workshop on Logical Frameworks and Meta-Languages, Informal Proceedings},
  year      = {2004},
  ee        = {http://www.tcs.informatik.uni-muenchen.de/~abel},
}


@inproceedings{Doczkal:09,
 author = {Doczkal, Christian and Schwinghammer, Jan},
 title = { {Formalizing a Strong Normalization proof for Moggi's Computational Metalanguage: A Case Study in Isabelle/HOL-Nominal} },
 booktitle = {LFMTP '09: Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages},
 year = {2009},
 isbn = {978-1-60558-529-1},
 pages = {57--63},
 location = {Montreal, Quebec, Canada},
 doi = {http://doi.acm.org/10.1145/1577824.1577834},
 publisher = {ACM},
 address = {New York, NY, USA},
 }
