@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},
)