@article(APTS13,
 author       = {Andreas Abel and Brigitte Pientka and David Thibodeau and Anton Setzer},
 year         = {2013},
 title        = {Copatterns: Programming Infinite Structures by Observations},
 journal      = {SIGPLAN Not.},
 volume       = {48},
 number       = {1},
 pages        = {27\IeC{\textendash}38},
 doi          = {10.1145/2480359.2429075},
)
@inproceedings(AP13,
 author       = {Andreas M. Abel and Brigitte Pientka},
 year         = {2013},
 title        = {Wellfounded Recursion with Copatterns: A Unified Approach to Termination and Productivity},
 booktitle    = {Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming},
 series       = {ICFP \IeC{\textquoteright}13},
 publisher    = {Association for Computing Machinery},
 address      = {New York, NY, USA},
 pages        = {185\IeC{\textendash}196},
 doi          = {10.1145/2500365.2500591},
)
@article(ABCEKLM06,
 author       = {Stuart F. Allen and Mark Bickford and Robert L. Constable and Richard Eaton and Christoph Kreitz and Lori Lorigo and E. Moran},
 year         = {2006},
 title        = {Innovations in computational type theory using {N}uprl},
 journal      = {J. Applied Logic},
 volume       = {4},
 number       = {4},
 pages        = {428--469},
 doi          = {10.1016/j.jal.2005.10.005},
)
@article(BFGPU00,
 author       = {Gilles Barthe and Maria Jo{\~{a}}o Frade and Eduardo Gim{\'{e}}nez and Lu{\'{\i}}s Pinto and Tarmo Uustalu},
 year         = {2004},
 title        = {Type-based termination of recursive definitions},
 journal      = {Mathematical Structures in Computer Science},
 volume       = {14},
 number       = {1},
 pages        = {97--141},
 doi          = {10.1017/S0960129503004122},
)
@article(BEPW16,
 author       = {Joachim Breitner and Richard A. Eisenberg and {Peyton Jones}, Simon and Stephanie Weirich},
 year         = {2016},
 title        = {Safe zero-cost coercions for Haskell},
 journal      = {J. Funct. Program.},
 volume       = {26},
 pages        = {e15},
 doi          = {10.1017/S0956796816000150},
)
@article(BDPR79,
 author       = {{C. B\"ohm and M. Dezani-Ciancaglini and P. Peretti and S.Ronchi Della Rocca}},
 year         = {1979},
 title        = {A discrimination algorithm inside \IeC{\ensuremath{\lambda}}-\IeC{\ensuremath{\beta}}-calculus},
 journal      = {Theoretical Computer Science},
 volume       = {8},
 number       = {3},
 pages        = {271 -- 291},
 doi          = {10.1016/0304-3975(79)90014-8},
)
@article(CH88,
 author       = {Thierry Coquand and G\IeC{\'e}rard Huet},
 year         = {1988},
 title        = {The calculus of constructions},
 journal      = {Information and Computation},
 volume       = {76},
 number       = {2/3},
 pages        = {95 -- 120},
 doi          = {10.1016/0890-5401(88)90005-3},
)
@inproceedings(FBS18,
 author       = {Denis Firsov and Richard Blair and Aaron Stump},
 year         = {2018},
 title        = {Efficient {M}endler-Style Lambda-Encodings in {C}edille},
 editor       = {Jeremy Avigad and Assia Mahboubi},
 booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP} 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {10895},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 pages        = {235--252},
 doi          = {10.1007/978-3-319-94821-8\_14},
)
@misc(FDJS18,
 author       = {Denis Firsov and Larry Diehl and Christopher Jenkins and Aaron Stump},
 year         = {2018},
 title        = {Course-of-Value Induction in Cedille},
 url          = {https://arxiv.org/abs/1811.11961},
 note         = {(manuscript)},
)
@inproceedings(FS18,
 author       = {Denis Firsov and Aaron Stump},
 year         = {2018},
 title        = {Generic Derivation of Induction for Impredicative Encodings in Cedille},
 booktitle    = {Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs},
 series       = {CPP 2018},
 publisher    = {Association for Computing Machinery},
 address      = {New York, NY, USA},
 pages        = {215\IeC{\textendash}227},
 doi          = {10.1145/3167087},
 url          = {https://doi-org.proxy.lib.uiowa.edu/10.1145/3167087},
)
@inproceedings(Ge92,
 author       = {Herman Geuvers},
 year         = {1992},
 title        = {Inductive and Coinductive types with Iteration and Recursion},
 editor       = {Nordstr\IeC{\"o}m, B. and K. Pettersson and G. Plotkin},
 booktitle    = {Informal Proceedings of the Workshop on Types for Proofs and Programs, {TYPES} '92},
 organization = {Dept of Computing Science, Chalmers Univ. of Tehnology and G\"oteborg Univ.},
 pages        = {193--217},
 url          = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.35.9758},
)
@inproceedings(Geu01,
 author       = {Herman Geuvers},
 year         = {2001},
 title        = {Induction Is Not Derivable in Second Order Dependent Type Theory},
 editor       = {Samson Abramsky},
 booktitle    = {International Conference on Typed Lambda Calculi and Applications},
 publisher    = {Springer},
 address      = {Berlin, Heidelberg},
 pages        = {166--181},
 doi          = {10.1007/3-540-45413-6_16},
)
@unpublished(Ge14,
 author       = {Herman Geuvers},
 year         = {2014},
 title        = {The Church-Scott representation of inductive and coinductive data},
 url          = {http://citeseerx.ist.psu.edu/viewdoc/citations?doi=10.1.1.705.2662},
 note         = {(manuscript)},
)
@phdthesis(Ha87,
 author       = {Tatsuya Hagino},
 year         = {1987},
 title        = {A categorical programming language},
 school       = {The University of Edinburgh},
)
@misc(JS20,
 author       = {Christopher Jenkins and Aaron Stump},
 year         = {2020},
 title        = {Monotone recursive types and recursive data representations in Cedille},
 url          = {https://arxiv.org/abs/2001.02828},
 note         = {(manuscript)},
)
@inproceedings(Kop03,
 author       = {Alexei Kopylov},
 year         = {2003},
 title        = {Dependent Intersection: {A} New Way of Defining Records in Type Theory},
 booktitle    = {Proceedings of 18th {IEEE} Symposium on Logic in Computer Science {(LICS} 2003), 22-25 June 2003, Ottawa, Canada},
 series       = {LICS '03},
 publisher    = {{IEEE} Computer Society},
 pages        = {86--95},
 doi          = {10.1109/LICS.2003.1210048},
)
@article(Lam68,
 author       = {Joachim Lambek},
 year         = {1968},
 title        = {A Fixpoint Theorem for Complete Categories},
 journal      = {Mathematische Zeitschrift},
 volume       = {103},
 number       = {2},
 pages        = {151--161},
 doi          = {10.1007/bf01110627},
)
@inproceedings(Lei89,
 author       = {Daniel Leivant},
 year         = {1989},
 title        = {Contracting proofs to programs},
 editor       = {P. Odifreddi},
 booktitle    = {Logic and Computer Science},
 pages        = {279--327},
 doi          = {10.1184/R1/6604463.v1},
)
@phdthesis(Mat98b,
 author       = {Ralph Matthes},
 year         = {1998},
 title        = {{Extensions of System F by Iteration and Primitive Recursion on Monotone Inductive Types}},
 school       = {Ludwig-Maximilians-Universit{\"a}t M{\"u}nchen},
)
@inproceedings(Mat98,
 author       = {Ralph Matthes},
 year         = {1998},
 title        = {Monotone Fixed-Point Types and Strong Normalization},
 editor       = {Georg Gottlob and Etienne Grandjean and Katrin Seyr},
 booktitle    = {Computer Science Logic, 12th International Workshop, {CSL} '98, Annual Conference of the EACSL, Brno, Czech Republic, August 24-28, 1998, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {1584},
 publisher    = {Springer},
 pages        = {298--312},
 doi          = {10.1007/10703163\_20},
)
@article(Mat99,
 author       = {Ralph Matthes},
 year         = {1999},
 title        = {Monotone (co)inductive types and positive fixed-point types},
 journal      = {RAIRO - Theoretical Informatics and Applications},
 volume       = {33},
 number       = {4-5},
 pages        = {309\IeC{\textendash}328},
 doi          = {10.1051/ita:1999120},
)
@inproceedings(Men87,
 author       = {N. P. Mendler},
 year         = {1987},
 title        = {Recursive Types and Type Constraints in Second-Order Lambda Calculus},
 booktitle    = {Proceedings of the Symposium on Logic in Computer Science},
 series       = {(LICS '87)},
 publisher    = {{IEEE} Computer Society},
 address      = {Los Alamitos, CA},
 pages        = {30--36},
)
@inproceedings(Men91,
 author       = {N. P. {Mendler}},
 year         = {1991},
 title        = {Predictive type universes and primitive recursion},
 booktitle    = {Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science},
 series       = {LICS '91},
 pages        = {173--184},
 doi          = {10.1109/LICS.1991.151642},
)
@article(Me91,
 author       = {Nax Paul Mendler},
 year         = {1991},
 title        = {Inductive types and type constraints in the second-order lambda calculus},
 journal      = {Annals of Pure and Applied Logic},
 volume       = {51},
 number       = {1},
 pages        = {159 -- 172},
 doi          = {10.1016/0168-0072(91)90069-X},
)
@inproceedings(Mi01,
 author       = {Alexandre Miquel},
 year         = {2001},
 title        = {The Implicit Calculus of Constructions: Extending Pure Type Systems with an Intersection Type Binder and Subtyping},
 booktitle    = {Proceedings of the 5th International Conference on Typed Lambda Calculi and Applications},
 series       = {TLCA\IeC{\textquoteright}01},
 publisher    = {Springer-Verlag},
 address      = {Berlin, Heidelberg},
 pages        = {344\IeC{\textendash}359},
 doi          = {10.1007/3-540-45413-6\_27},
 url          = {http://dl.acm.org/citation.cfm?id=1754621.1754650},
)
@inproceedings(Par88,
 author       = {Michel Parigot},
 year         = {1988},
 title        = {Programming with Proofs: {A} Second Order Type Theory},
 editor       = {Harald Ganzinger},
 booktitle    = {{ESOP} '88, 2nd European Symposium on Programming, Nancy, France, March 21-24, 1988, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {300},
 publisher    = {Springer},
 address      = {Berlin, Heidelberg},
 pages        = {145--159},
 doi          = {10.1007/3-540-19027-9\_10},
)
@inproceedings(Par89,
 author       = {Michel Parigot},
 year         = {1989},
 title        = {On the Representation of Data in Lambda-Calculus},
 editor       = {Egon B{\"{o}}rger and Hans Kleine B{\"{u}}ning and Michael M. Richter},
 booktitle    = {{CSL} '89, 3rd Workshop on Computer Science Logic, Kaiserslautern, Germany, October 2-6, 1989, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {440},
 publisher    = {Springer},
 address      = {Berlin, Heidelberg},
 pages        = {309--321},
 doi          = {10.1007/3-540-52753-2\_47},
)
@inproceedings(Pit98,
 author       = {Andrew M. Pitts},
 year         = {1998},
 title        = {Existential Types: Logical Relations and Operational Equivalence},
 editor       = {Kim Guldstrand Larsen and Sven Skyum and Glynn Winskel},
 booktitle    = {Automata, Languages and Programming, 25th International Colloquium, ICALP'98, Aalborg, Denmark, July 13-17, 1998, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {1443},
 publisher    = {Springer},
 pages        = {309--326},
 doi          = {10.1007/BFb0055063},
)
@inproceedings(SU99,
 author       = {Zdzislaw Splawski and Pawel Urzyczyn},
 year         = {1999},
 title        = {Type Fixpoints: Iteration vs. Recursion},
 editor       = {Didier R{\'{e}}my and Peter Lee},
 booktitle    = {Proceedings of the fourth {ACM} {SIGPLAN} International Conference on Functional Programming {(ICFP} '99), Paris, France, September 27-29, 1999},
 publisher    = {{ACM}},
 pages        = {102--113},
 doi          = {10.1145/317636.317789},
)
@article(Stu17,
 author       = {Aaron Stump},
 year         = {2017},
 title        = {The calculus of dependent lambda eliminations},
 journal      = {J. Funct. Program.},
 volume       = {27},
 pages        = {e14},
 doi          = {10.1017/S0956796817000053},
)
@article(Stu18a,
 author       = {Aaron Stump},
 year         = {2018},
 title        = {From realizability to induction via dependent intersection},
 journal      = {Ann. Pure Appl. Logic},
 volume       = {169},
 number       = {7},
 pages        = {637--655},
 doi          = {10.1016/j.apal.2018.03.002},
)
@unpublished(Stu18b,
 author       = {Aaron Stump},
 year         = {2018},
 title        = {Syntax and Semantics of Cedille},
 url          = {http://arxiv.org/abs/1806.04709},
)
@unpublished(Stu18c,
 author       = {Aaron Stump},
 year         = {2018},
 title        = {Syntax and Typing for Cedille Core},
 url          = {http://arxiv.org/abs/1811.01318},
)
@article(Tar55,
 author       = {Alfred Tarski},
 year         = {1955},
 title        = {A lattice-theoretical fixpoint theorem and its applications},
 journal      = {Pacific Journal of Mathematics},
 volume       = {5},
 number       = {2},
 pages        = {285--309},
 doi          = {10.2140/pjm.1955.5.285},
)
@article(UV99,
 author       = {Tarmo Uustalu and Varmo Vene},
 year         = {1999},
 title        = {Mendler-style Inductive Types, Categorically},
 journal      = {Nordic J. of Computing},
 volume       = {6},
 number       = {3},
 pages        = {343--361},
 url          = {http://dl.acm.org/citation.cfm?id=774455.774462},
)
@inproceedings(UV00,
 author       = {Tarmo Uustalu and Varmo Vene},
 year         = {2000},
 title        = {Coding Recursion a la {M}endler (Extended Abstract)},
 booktitle    = {Proc. of the 2nd Workshop on Generic Programming, WGP 2000, Technical Report {UU-CS-2000-19}},
 organization = {Dept. of Computer Science, Utrecht University},
 pages        = {69--85},
)
@phdthesis(Ven00,
 author       = {Varmo Vene},
 year         = {2000},
 title        = {Categorical programming with inductive and coinductive types},
 school       = {University of Tartu},
)
@unpublished(Wad90,
 author       = {Philip Wadler},
 year         = {1990},
 title        = {Recursive Types for Free!},
 url          = {https://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt},
 note         = {Unpublished},
)
@phdthesis(We94,
 author       = {Benjamin Werner},
 year         = {1994},
 title        = {Une th{\'e}orie des constructions inductives},
 school       = {Universit\'e Paris-Diderot},
)