@article(abelAlti:predicative,
 author       = "Andreas Abel and Thorsten Altenkirch",
 year         = "2002",
 title        = "A Predicative Analysis of Structural Recursion",
 journal      = "J. Func. Program.",
 volume       = "12",
 number       = "1",
 pages        = "1--41",
 doi          = "10.1017/S0956796801004191",
)
@phdthesis(abel:PhD,
 author       = "Andreas Abel",
 year         = "2006",
 title        = "A Polymorphic Lambda-Calculus with Sized Higher-Order Types",
 type         = "Ph.D. thesis",
 school       = "Ludwig-Maximilians-Universit\"at M\"unchen",
)
@inproceedings(abel:aplas07,
 author       = "Andreas Abel",
 year         = "2007",
 title        = "Mixed Inductive/Coinductive Types and Strong Normalization",
 editor       = "Zhong Shao",
 booktitle    = "Proc. of the 5th Asian Symp. on Programming Languages and Systems, APLAS 2007",
 series       = "Lect. Notes in Comput. Sci.",
 volume       = "4807",
 publisher    = "Springer",
 pages        = "286--301",
 doi          = "10.1007/978-3-540-76637-7\_19",
)
@article(abel:mscs06,
 author       = "Andreas Abel",
 year         = "2008",
 title        = "Polarized Subtyping for Sized Types",
 journal      = "Math. Struct. in Comput. Sci.",
 volume       = "18",
 pages        = "797--822",
 doi          = "10.1017/S0960129508006853",
 note         = "Special issue on subtyping, edited by Healfdene Goguen and Adriana Compagnoni.",
)
@article(abel:lmcs07,
 author       = "Andreas Abel",
 year         = "2008",
 title        = "Semi-continuous Sized Types and Termination",
 journal      = "Logical Meth. in Comput. Sci.",
 volume       = "4",
 number       = "2",
 doi          = "10.2168/LMCS-4(2:3)2008",
 note         = "CSL'06 special issue.",
)
@inproceedings(abel:par10,
 author       = "Andreas Abel",
 year         = "2010",
 title        = "{MiniAgda}: {I}ntegrating Sized and Dependent Types",
 editor       = "Ana Bove and Ekaterina Komendantskaya and Milad Niqui",
 booktitle    = "Wksh. on Partiality And Recursion in Interactive Theorem Provers (PAR 2010)",
 series       = "Electr. Proc. in Theor. Comp. Sci.",
 volume       = "43",
 pages        = "14--28",
 doi          = "10.4204/EPTCS.43.2",
)
@inproceedings(abel:fossacs11,
 author       = "Andreas Abel",
 year         = "2011",
 title        = "Irrelevance in Type Theory with a Heterogeneous Equality Judgement",
 editor       = "Martin Hofmann",
 booktitle    = "Proc. of the 14th Int. Conf. on Foundations of Software Science and Computational Structures, FOSSACS 2011",
 series       = "Lect. Notes in Comput. Sci.",
 volume       = "6604",
 publisher    = "Springer",
 pages        = "57--71",
 doi          = "10.1007/978-3-642-19805-2\_5",
)
@article(aspinallCompagnoni:tcs01,
 author       = "David Aspinall and Adriana B. Compagnoni",
 year         = "2001",
 title        = "Subtyping dependent types",
 journal      = "Theor. Comput. Sci.",
 volume       = "266",
 number       = "1-2",
 pages        = "273--309",
 doi          = "10.1016/S0304-3975(00)00175-4",
)
@inproceedings(amadio:guardcondition,
 author       = "Roberto M. Amadio and Solange Coupet-Grimal",
 year         = "1998",
 title        = "Analysis of a Guard Condition in Type Theory (Extended Abstract).",
 editor       = "Maurice Nivat",
 booktitle    = "Proc. of the 1st Int. Conf. on Foundations of Software Science and Computation Structure, FoSSaCS'98",
 series       = "Lect. Notes in Comput. Sci.",
 volume       = "1378",
 publisher    = "Springer",
 pages        = "48--62",
 doi          = "10.1007/BFb0053541",
)
@misc(altenkirchDanielsson:par10,
 author       = "Thorsten Altenkirch and Nils Anders Danielsson",
 year         = "2010",
 title        = "Termination Checking in the Presence of Nested Inductive and Coinductive Types",
 howpublished = "Short note supporting a talk given at PAR 2010, Workshop on Partiality and Recursion in Interactive Theorem Provers, FLoC 2010",
 url          = "http://www.cse.chalmers.se/~nad/publications/altenkirch-danielsson-par2010.pdf",
)
@inproceedings(alti:flops10,
 author       = "Thorsten Altenkirch and Nils Anders Danielsson and Andres L{\"o}h and Nicolas Oury",
 year         = "2010",
 title        = "PiSigma: Dependent Types without the Sugar",
 editor       = "Matthias Blume and Naoki Kobayashi and Germ{\'a}n Vidal",
 booktitle    = "Proc. of the 10th Int. Symp. on Functional and Logic Programming, FLOPS 2010",
 series       = "Lect. Notes in Comput. Sci.",
 volume       = "6009",
 publisher    = "Springer",
 pages        = "40--55",
 doi          = "10.1007/978-3-642-12251-4\_5",
)
@inproceedings(altenkirchMcBrideSwierstra:plpv07,
 author       = "Thorsten Altenkirch and Conor McBride and Wouter Swierstra",
 year         = "2007",
 title        = "Observational equality, now!",
 editor       = "Aaron Stump and Hongwei Xi",
 booktitle    = "Proc. of the Wksh. Programming Languages meets Program Verification, PLPV 2007",
 publisher    = "ACM Press",
 pages        = "57--68",
 doi          = "10.1145/1292597.1292608",
)
@book(aczelRathjen:constructiveSetTheory,
 author       = "Peter Aczel and Michael Rathjen",
 year         = "2008",
 title        = "Notes on Constructive Set Theory",
 url          = "http://www.maths.manchester.ac.uk/logic/mathlogaps/workshop/CST-book-June-08.pdf",
 note         = "Draft.",
)
@phdthesis(barras:PhD,
 author       = "Bruno Barras",
 year         = "1999",
 title        = "Auto-validation d'un syst\`eme de preuves avec familles inductives",
 type         = "Ph.D. thesis",
 school       = "Universit\'e Paris 7",
)
@article(barras:jfr10,
 author       = "Bruno Barras",
 year         = "2010",
 title        = "Sets in Coq, Coq in Sets",
 journal      = "J. Formalized Reasoning",
 volume       = "3",
 number       = "1",
 url          = "http://jfr.cib.unibo.it/article/view/1695",
)
@misc(barras:jfla10,
 author       = "Bruno Barras",
 year         = "2010",
 title        = "The syntactic guard condition of Coq",
 howpublished = "Talk at the Journ\'ee ``\'egalit\'e et terminaison'' du 2 f\'evrier 2010 in conjunction with JFLA 2010",
 url          = "http://coq.inria.fr/files/adt-2fev10-barras.pdf",
)
@inproceedings(barrasBernardo:fossacs08,
 author       = "Bruno Barras and Bruno Bernardo",
 year         = "2008",
 title        = "The Implicit Calculus of Constructions as a Programming Language with Dependent Types",
 editor       = "Roberto M. Amadio",
 booktitle    = "FoSSaCS",
 series       = "Lect. Notes in Comput. Sci.",
 volume       = "4962",
 publisher    = "Springer",
 pages        = "365--379",
 doi          = "10.1007/978-3-540-78499-9\_26",
)
@inproceedings(bartheGregoirePastawski:lpar06,
 author       = "Gilles Barthe and Benjamin Gr{\'e}goire and Fernando Pastawski",
 year         = "2006",
 title        = "{CIC\^{}}: Type-Based Termination of Recursive Definitions in the {C}alculus of {I}nductive {C}onstructions",
 editor       = "Miki Hermann and Andrei Voronkov",
 booktitle    = "Proc. of the 13th Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2006",
 series       = "Lect. Notes in Comput. Sci.",
 volume       = "4246",
 publisher    = "Springer",
 pages        = "257--271",
 doi          = "10.1007/11916277\_18",
)
@inproceedings(bartheGregoireRiba:lernet08,
 author       = "Gilles Barthe and Benjamin Gr{\'e}goire and Colin Riba",
 year         = "2008",
 title        = "A Tutorial on Type-Based Termination",
 editor       = "Ana Bove and Lu\'{\i }s Soares Barbosa and Alberto Pardo and Jorge Sousa Pinto",
 booktitle    = "LerNet ALFA Summer School",
 series       = "Lect. Notes in Comput. Sci.",
 volume       = "5520",
 publisher    = "Springer",
 pages        = "100--152",
 doi          = "10.1007/978-3-642-03153-3\_3",
)
@inproceedings(bartheGregoireRiba:csl08,
 author       = "Gilles Barthe and Benjamin Gr{\'e}goire and Colin Riba",
 year         = "2008",
 title        = "Type-Based Termination with Sized Products",
 editor       = "Michael Kaminski and Simone Martini",
 booktitle    = "Computer Science Logic, 22nd Int. Wksh., CSL 2008, 17th Annual Conf. of the EACSL",
 series       = "Lect. Notes in Comput. Sci.",
 volume       = "5213",
 publisher    = "Springer",
 pages        = "493--507",
 doi          = "10.1007/978-3-540-87531-4\_35",
)
@inproceedings(blanqui:rta04,
 author       = "Fr\'ed\'eric Blanqui",
 year         = "2004",
 title        = "A Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite Systems",
 editor       = "Vincent van Oostrom",
 booktitle    = "Rewriting Techniques and Applications (RTA 2004), Aachen, Germany",
 series       = "Lect. Notes in Comput. Sci.",
 volume       = "3091",
 publisher    = "Springer",
 pages        = "24--39",
 doi          = "10.1007/978-3-540-25979-4\_2",
)
@article(cousot:constructiveTarski,
 author       = "Patrick Cousot and Radhia Cousot",
 year         = "1979",
 title        = "Constructive Versions of {T}arski's Fixed Point Theorems",
 journal      = "Pacific Journal of Mathematics",
 volume       = "81",
 number       = "1",
 pages        = "43--57",
)
@inproceedings(chen:subtypingCC,
 author       = "Gang Chen",
 year         = "1997",
 title        = "Subtyping Calculus of Construction (Extended Abstract)",
 editor       = "Igor Pr\'{\i }vara and Peter Ruzicka",
 booktitle    = "Proc. of the 22nd Int. Symb. on Mathematical Foundations of Computer Science, MFCS'97",
 series       = "Lect. Notes in Comput. Sci.",
 volume       = "1295",
 publisher    = "Springer",
 pages        = "189--198",
 doi          = "10.1007/BFb0029962",
)
@inproceedings(chen:popl03,
 author       = "Gang Chen",
 year         = "2003",
 title        = "Coercive subtyping for the calculus of constructions",
 booktitle    = "Proc. of the 30st ACM Symp. on Principles of Programming Languages, POPL 2003",
 series       = "ACM SIGPLAN Notices",
 volume       = "38",
 publisher    = "ACM Press",
 pages        = "150--159",
 doi          = "10.1145/640128.604145",
)
@inproceedings(coquand:infiniteObjects,
 author       = "Thierry Coquand",
 year         = "1993",
 title        = "Infinite Objects in Type Theory",
 editor       = "H. Barendregt and T. Nipkow",
 booktitle    = "Types for Proofs and Programs (TYPES '93)",
 series       = "Lect. Notes in Comput. Sci.",
 volume       = "806",
 publisher    = "Springer",
 pages        = "62--78",
 doi          = "10.1007/3-540-58085-9\_72",
)
@inproceedings(danielssonAltenkirch:mpc10,
 author       = "Nils Anders Danielsson and Thorsten Altenkirch",
 year         = "2010",
 title        = "Subtyping, Declaratively",
 editor       = "Claude Bolduc and Jules Desharnais and B{\'e}chir Ktari",
 booktitle    = "Proc. of the 10th Int. Conf. on Mathematics of Program Construction, MPC 2010",
 series       = "Lect. Notes in Comput. Sci.",
 volume       = "6120",
 publisher    = "Springer",
 pages        = "100--118",
 doi          = "10.1007/978-3-642-13321-3\_8",
)
@article(damGurov:jlc02,
 author       = "Mads Dam and Dilian Gurov",
 year         = "2002",
 title        = "$\mu $-Calculus with Explicit Points and Approximations",
 journal      = "J. Log. Comput.",
 volume       = "12",
 number       = "2",
 pages        = "255--269",
 doi          = "10.1093/logcom/12.2.255",
)
@phdthesis(frade:PhD,
 author       = "Maria {Jo\~{a}o} Frade",
 year         = "2003",
 title        = "Type-Based Termination of Recursive Definitions and Constructor Subtyping in Typed Lambda Calculi",
 type         = "Ph.D. thesis",
 school       = "Universidade do Minho, Departamento de Inform\'{a}tica",
)
@article(ghaniHancockPattinson:entcs06,
 author       = "Neil Ghani and Peter Hancock and Dirk Pattinson",
 year         = "2006",
 title        = "Continuous Functions on Final Coalgebras",
 journal      = "Electr. Notes in Theor. Comp. Sci.",
 volume       = "164",
 number       = "1",
 pages        = "141--155",
 doi          = "10.1016/j.entcs.2006.06.009",
)
@article(ghaniHancockPattinson:lmcs09,
 author       = "Neil Ghani and Peter Hancock and Dirk Pattinson",
 year         = "2009",
 title        = "Representations of Stream Processors Using Nested Fixed Points",
 journal      = "Logical Meth. in Comput. Sci.",
 volume       = "5",
 number       = "3",
 doi          = "10.2168/LMCS-5(3:9)2009",
)
@inproceedings(gimenez:guardeddefinitions,
 author       = "Eduardo Gim\'enez",
 year         = "1995",
 title        = "Codifying Guarded Definitions with Recursive Schemes",
 editor       = "Peter Dybjer and Bengt Nordstr\"{o}m and Jan Smith",
 booktitle    = "Types for Proofs and Programs, Int. Wksh., TYPES'94",
 series       = "Lect. Notes in Comput. Sci.",
 volume       = "996",
 publisher    = "Springer",
 pages        = "39--59",
 doi          = "10.1007/3-540-60579-7\_3",
)
@inproceedings(gimenez:strec,
 author       = "Eduardo Gim\'enez",
 year         = "1998",
 title        = "Structural Recursive Definitions in Type Theory",
 editor       = "K. G. Larsen and S. Skyum and G. Winskel",
 booktitle    = "Int. Colloquium on Automata, Languages and Programming (ICALP'98), Aalborg, Denmark",
 series       = "Lect. Notes in Comput. Sci.",
 volume       = "1443",
 publisher    = "Springer",
 pages        = "397--408",
 doi          = "10.1007/BFb0055070",
)
@phdthesis(girard:thesis,
 author       = "Jean-Yves Girard",
 year         = "1972",
 title        = "Interpr{\'e}tation fonctionnelle et {\'e}limination des coupures dans l'arithm{\'e}tique d'ordre sup{\'e}rieur",
 type         = "Th{\`e}se de {D}octorat {d'{\'E}tat}",
 school       = "Universit{\'e} de Paris VII",
)
@inproceedings(hughesParetoSabry:popl96,
 author       = "John Hughes and Lars Pareto and Amr Sabry",
 year         = "1996",
 title        = "Proving the Correctness of Reactive Systems Using Sized Types",
 booktitle    = "Proc. of the 23rd ACM Symp. on Principles of Programming Languages, POPL'96",
 pages        = "410--423",
 doi          = "10.1145/237721.240882",
)
@inproceedings(hutchins:popl10,
 author       = "DeLesley S. Hutchins",
 year         = "2010",
 title        = "Pure subtype systems",
 editor       = "Manuel V. Hermenegildo and Jens Palsberg",
 booktitle    = "Proc. of the 37th ACM Symp. on Principles of Programming Languages, POPL 2010",
 publisher    = "ACM Press",
 pages        = "287--298",
 doi          = "10.1145/1706299.1706334",
)
@manual(inria:coq83,
 author       = "INRIA",
 year         = "2010",
 title        = "The Coq Proof Assistant Reference Manual",
 edition      = "version 8.3",
 organization = "INRIA",
 url          = "http://coq.inria.fr/",
)
@article(luoAdams:mscs08,
 author       = "Zhaohui Luo and Robin Adams",
 year         = "2008",
 title        = "Structural subtyping for inductive types with functorial equality rules",
 journal      = "Math. Struct. in Comput. Sci.",
 volume       = "18",
 number       = "5",
 pages        = "931--972",
 doi          = "10.1017/S0960129508006956",
)
@inproceedings(mcBride:calco09,
 author       = "Conor McBride",
 year         = "2009",
 title        = "Let's See How Things Unfold: Reconciling the Infinite with the Intensional",
 editor       = "Alexander Kurz and Marina Lenisa and Andrzej Tarlecki",
 booktitle    = "3rd Int. Conf. on Algebra and Coalgebra in Computer Science, CALCO 2009",
 series       = "Lect. Notes in Comput. Sci.",
 volume       = "5728",
 publisher    = "Springer",
 pages        = "113--126",
 doi          = "10.1007/978-3-642-03741-2\_9",
)
@inproceedings(mendler:lics,
 author       = "Nax Paul Mendler",
 year         = "1987",
 title        = "Recursive Types and Type Constraints in Second-Order Lambda Calculus",
 booktitle    = "Proc. of the 2nd IEEE Symp. on Logic in Computer Science (LICS'87)",
 publisher    = "IEEE Computer Soc. Press",
 pages        = "30--36",
)
@article(milner:goWrong,
 author       = "Robin Milner",
 year         = "1978",
 title        = "A Theory of Type Polymorphism in Programming",
 journal      = "J. Comput. Syst. Sci.",
 volume       = "17",
 pages        = "348--375",
 doi          = "10.1016/0022-0000(78)90014-4",
)
@phdthesis(norell:PhD,
 author       = "Ulf Norell",
 year         = "2007",
 title        = "Towards a Practical Programming Language Based on Dependent Type Theory",
 type         = "Ph.D. thesis",
 school       = "Dept of Comput. Sci. and Engrg., Chalmers",
 address      = "G\"{o}teborg, Sweden",
)
@phdthesis(pareto:PhD,
 author       = "Lars Pareto",
 year         = "2000",
 title        = "Types for Crash Prevention",
 type         = "Ph.D. thesis",
 school       = "Chalmers University of Technology",
)
@inproceedings(pientka:termination,
 author       = "Brigitte Pientka",
 year         = "2001",
 title        = "Termination and Reduction Checking for Higher-Order Logic Programs",
 editor       = "Rajeev Gor\'{e} and Alexander Leitsch and Tobias Nipkow",
 booktitle    = "Automated Reasoning, First International Joint Conference, IJCAR 2001",
 series       = "Lect. Notes in Art. Intell.",
 volume       = "2083",
 publisher    = "Springer",
 pages        = "401--415",
 doi          = "10.1007/3-540-45744-5\_32",
)
@article(qianNipkow:jar94,
 author       = "Zhenyu Qian and Tobias Nipkow",
 year         = "1994",
 title        = "Reduction and Unification in Lambda Calculi with a General Notion of Subtype",
 journal      = "J. of Autom. Reasoning",
 volume       = "12",
 number       = "3",
 pages        = "389--406",
 doi          = "10.1007/BF00885767",
)
@inproceedings(reynolds:systemF,
 author       = "John C. Reynolds",
 year         = "1974",
 title        = "Towards a Theory of Type Structure",
 editor       = "B. Robinet",
 booktitle    = "Programming Symposium",
 series       = "Lect. Notes in Comput. Sci.",
 volume       = "19",
 publisher    = "Springer",
 address      = "Berlin",
 pages        = "408--425",
 doi          = "10.1007/3-540-06859-7\_148",
)
@phdthesis(sacchini:PhD,
 author       = "Jorge Luis Sacchini",
 year         = "2011",
 title        = "On Type-Based Termination and Pattern Matching in the Calculus of Inductive Constructions",
 type         = "Ph.D. thesis",
 school       = "INRIA Sophia-Antipolis and \'Ecole des Mines de Paris",
)
@inproceedings(sprengerDam:fossacs03,
 author       = "Christoph Sprenger and Mads Dam",
 year         = "2003",
 title        = "On the Structure of Inductive Reasoning: Circular and Tree-Shaped Proofs in the $\mu $-Calculus",
 editor       = "Andrew D. Gordon",
 booktitle    = "Proc. of the 6th Int. Conf. on Foundations of Software Science and Computational Structures, FoSSaCS 2003",
 series       = "Lect. Notes in Comput. Sci.",
 volume       = "2620",
 publisher    = "Springer",
 pages        = "425--440",
 doi          = "10.1007/3-540-36576-1\_27",
)
@inproceedings(schoeppSimpson:fossacs02,
 author       = "Ulrich Sch{\"o}pp and Alex K. Simpson",
 year         = "2002",
 title        = "Verifying Temporal Properties Using Explicit Approximants: Completeness for Context-free Processes",
 editor       = "Mogens Nielsen and Uffe Engberg",
 booktitle    = "Proc. of the 5th Int. Conf. on Foundations of Software Science and Computational Structures, FoSSaCS 2002",
 series       = "Lect. Notes in Comput. Sci.",
 volume       = "2303",
 publisher    = "Springer",
 pages        = "372--386",
 doi          = "10.1007/3-540-45931-6\_26",
)
@phdthesis(steffen:PhD,
 author       = "Martin Steffen",
 year         = "1998",
 title        = "Polarized Higher-Order Subtyping",
 type         = "Ph.D. thesis",
 school       = "Technische Fakult{\"a}t, Universit{\"a}t Erlangen",
)
@article(tait:functionalsFiniteTypeI,
 author       = "William W. Tait",
 year         = "1967",
 title        = "Intensional Interpretations of Functionals of Finite Type {I}",
 journal      = "J. Symb. Logic",
 volume       = "32",
 number       = "2",
 pages        = "198--212",
)
@mastersthesis(wahlstedt:master,
 author       = "David Wahlstedt",
 year         = "2000",
 title        = "Detecting termination using size-change in parameter values",
 type         = "Master's thesis",
 school       = "G{\"o}teborgs Universitet",
)
@article(xi:terminationHOSC,
 author       = "Hongwei Xi",
 year         = "2002",
 title        = "Dependent Types for Program Termination Verification",
 journal      = "J. Higher-Order and Symb. Comput.",
 volume       = "15",
 number       = "1",
 pages        = "91--131",
 doi          = "10.1023/A:1019916231463",
)