@inproceedings(Abel:2006,
 author       = "Andreas Abel",
 year         = "2006",
 title        = "Implementing a normalizer using sized heterogeneous types",
 booktitle    = "In Workshop on Mathematically Structured Functional Programming, MSFP",
 doi          = "10.1017/S0956796809007266",
)
@inproceedings(Abel:2008,
 author       = "Andreas Abel and Dulma Rodriguez",
 year         = "2008",
 title        = "Syntactic Metatheory of Higher-Order Subtyping",
 booktitle    = "Proceedings of the 22nd international workshop on Computer Science Logic",
 series       = "CSL '08",
 publisher    = "Springer-Verlag",
 address      = "Berlin, Heidelberg",
 pages        = "446--460",
 doi          = "10.1007/978-3-540-87531-4\_32",
)
@phdthesis(Adams:2004,
 author       = "Robin Adams",
 year         = "2004",
 title        = "A Modular Hierarchy of Logical Frameworks",
)
@book(Amadio:1998,
 author       = "R.M. Amadio and P.L. Curien",
 year         = "1998",
 title        = "Domains and lambda-calculi",
 series       = "Cambridge tracts in theoretical computer science",
 publisher    = "Cambridge University Press",
 doi          = "10.1017/CBO9780511983504",
)
@article(Barthe:1997,
 author       = "G. Barthe and J. Hatcliff and M. Heine S{\o }rensen",
 year         = "1997",
 title        = "A notion of classical pure type system (preliminary version)",
 journal      = "Electronic Notes in Theoretical Computer Science",
 volume       = "6",
 pages        = "4--59",
 doi          = "10.1016/S1571-0661(05)80170-7",
)
@article(Barthe:2001,
 author       = "Gilles Barthe and John Hatcliff and Morten Heine Sørensen",
 year         = "2001",
 title        = "Weak normalization implies strong normalization in a class of non-dependent pure type systems",
 journal      = "Theoretical Computer Science",
 volume       = "269",
 number       = "1-2",
 pages        = "317 -- 361",
 doi          = "10.1016/S0304-3975(01)00012-3",
)
@article(David:2003,
 author       = "Rene David and Karim Nour",
 year         = "2003",
 title        = "A short proof of the strong normalization of the simply typed lambdamu-calculus",
 journal      = "SCHEDAE INFORMATICAE",
 volume       = "12",
 pages        = "27--33",
)
@conference(Eades:2010,
 author       = "Harley Eades and Aaron Stump",
 year         = "2010",
 title        = "Hereditary Substitution for Stratified System F",
 booktitle    = "Proof-Search in Type Theories (PSTT)",
)
@book(Girard:1989,
 author       = "Jean-Yves Girard and Yves Lafont and Paul Taylor",
 year         = "1989",
 title        = "Proofs and Types (Cambridge Tracts in Theoretical Computer Science)",
 publisher    = "{Cambridge University Press}",
)
@unpublished(Eades:2011,
 author       = "Harley Eades II and Aaron Stump",
 year         = "2011",
 title        = "Using the Hereditary Substitution Function in Normalization Proofs",
 url          = "http://metatheorem.org/wp-content/papers/qual_companion_report.pdf",
)
@misc(Joachimski:1999,
 author       = "Felix Joachimski and Ralph Matthes",
 year         = "1999",
 title        = "Short Proofs of Normalization for the simply-typed lambda-calculus, permutative conversions and G{\"o}del's T",
)
@inproceedings(Keller:2010,
 author       = "Chantal Keller and Thorsten Altenkirch",
 year         = "2010",
 title        = "Hereditary substitutions for simple types, formalized",
 booktitle    = "Proceedings of the third ACM SIGPLAN workshop on Mathematically structured functional programming",
 series       = "MSFP '10",
 publisher    = "ACM",
 address      = "New York, NY, USA",
 pages        = "3--10",
 doi          = "10.1145/1863597.1863601",
)
@article(Leivant:1991,
 author       = "D. Leivant",
 year         = "1991",
 title        = "Finitely stratified polymorphism",
 journal      = "Inf. Comput.",
 volume       = "93",
 number       = "1",
 pages        = "93--113",
 doi          = "10.1016/0890-5401(91)90053-5",
)
@article(Levy:1976,
 author       = "Jean-Jacques L{\'e}vy",
 year         = "1976",
 title        = "An algebraic interpretation of the λβK-calculus; and an application of a labelled λ-calculus",
 journal      = "Theoretical Computer Science",
 volume       = "2",
 number       = "1",
 pages        = "97 -- 114",
 doi          = "10.1016/0304-3975(76)90009-8",
)
@incollection(Parigot:1992,
 author       = "Michel Parigot",
 year         = "1992",
 title        = "Lambda-Mu-Calculus: An algorithmic interpretation of classical natural deduction",
 editor       = "Andrei Voronkov",
 booktitle    = "Logic Programming and Automated Reasoning",
 series       = "Lecture Notes in Computer Science",
 volume       = "624",
 publisher    = "Springer Berlin / Heidelberg",
 pages        = "190--201",
 doi          = "10.1007/BFb0013061",
)
@article(Parigot:1997,
 author       = "Michel Parigot",
 year         = "1997",
 title        = "Proofs of Strong Normalization for Second Order Classical Natural Deduction",
 journal      = "Journal of Symbolic Logic",
 volume       = "62",
 number       = "4",
 pages        = "1461--1479",
 doi          = "10.2307/2275652",
)
@inproceedings(Rehof:1994,
 author       = "Jakob Rehof and Morten Heine S{\o }rensen",
 year         = "1994",
 title        = "The LambdaDelta-calculus",
 booktitle    = "Proceedings of the International Conference on Theoretical Aspects of Computer Software",
 series       = "TACS '94",
 publisher    = "Springer-Verlag",
 address      = "London, UK",
 pages        = "516--542",
 doi          = "10.1007/3-540-57887-0\_113",
)
@incollection(Watkins:2004,
 author       = "Kevin Watkins and Iliano Cervesato and Frank Pfenning and David Walker",
 year         = "2004",
 title        = "A Concurrent Logical Framework: The Propositional Fragment",
 editor       = "Stefano Berardi and Mario Coppo and Ferruccio Damiani",
 booktitle    = "Types for Proofs and Programs",
 series       = "Lecture Notes in Computer Science",
 volume       = "3085",
 publisher    = "Springer Berlin / Heidelberg",
 pages        = "355--377",
 doi          = "10.1007/978-3-540-24849-1\_23",
)