Andreas Abel, Brigitte Pientka, David Thibodeau & Anton Setzer (2013):
Copatterns: Programming Infinite Structures by Observations.
SIGPLAN Not. 48(1),
pp. 2738,
doi:10.1145/2480359.2429075.
Andreas M. Abel & Brigitte Pientka (2013):
Wellfounded Recursion with Copatterns: A Unified Approach to Termination and Productivity.
In: Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming,
ICFP 13.
Association for Computing Machinery,
New York, NY, USA,
pp. 185196,
doi:10.1145/2500365.2500591.
Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo & E. Moran (2006):
Innovations in computational type theory using Nuprl.
J. Applied Logic 4(4),
pp. 428–469,
doi:10.1016/j.jal.2005.10.005.
Gilles Barthe, Maria João Frade, Eduardo Giménez, Luís Pinto & Tarmo Uustalu (2004):
Type-based termination of recursive definitions.
Mathematical Structures in Computer Science 14(1),
pp. 97–141,
doi:10.1017/S0960129503004122.
Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones & Stephanie Weirich (2016):
Safe zero-cost coercions for Haskell.
J. Funct. Program. 26,
pp. e15,
doi:10.1017/S0956796816000150.
C. Böhm and M. Dezani-Ciancaglini and P. Peretti and S.Ronchi Della Rocca (1979):
A discrimination algorithm inside λ-β-calculus.
Theoretical Computer Science 8(3),
pp. 271 – 291,
doi:10.1016/0304-3975(79)90014-8.
Thierry Coquand & Gérard Huet (1988):
The calculus of constructions.
Information and Computation 76(2/3),
pp. 95 – 120,
doi:10.1016/0890-5401(88)90005-3.
Denis Firsov, Richard Blair & Aaron Stump (2018):
Efficient Mendler-Style Lambda-Encodings in Cedille.
In: Jeremy Avigad & Assia Mahboubi: 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,
Lecture Notes in Computer Science 10895.
Springer International Publishing,
Cham,
pp. 235–252,
doi:10.1007/978-3-319-94821-8_14.
Denis Firsov, Larry Diehl, Christopher Jenkins & Aaron Stump (2018):
Course-of-Value Induction in Cedille.
Available at https://arxiv.org/abs/1811.11961.
(manuscript).
Denis Firsov & Aaron Stump (2018):
Generic Derivation of Induction for Impredicative Encodings in Cedille.
In: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs,
CPP 2018.
Association for Computing Machinery,
New York, NY, USA,
pp. 215227,
doi:10.1145/3167087.
Available at https://doi-org.proxy.lib.uiowa.edu/10.1145/3167087.
Herman Geuvers (1992):
Inductive and Coinductive types with Iteration and Recursion.
In: B. Nordström, K. Pettersson & G. Plotkin: Informal Proceedings of the Workshop on Types for Proofs and Programs, TYPES '92.
Dept of Computing Science, Chalmers Univ. of Tehnology and Göteborg Univ.,
pp. 193–217.
Available at http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.35.9758.
Herman Geuvers (2001):
Induction Is Not Derivable in Second Order Dependent Type Theory.
In: Samson Abramsky: International Conference on Typed Lambda Calculi and Applications.
Springer,
Berlin, Heidelberg,
pp. 166–181,
doi:10.1007/3-540-45413-6_16.
Tatsuya Hagino (1987):
A categorical programming language.
The University of Edinburgh.
Christopher Jenkins & Aaron Stump (2020):
Monotone recursive types and recursive data representations in Cedille.
Available at https://arxiv.org/abs/2001.02828.
(manuscript).
Alexei Kopylov (2003):
Dependent Intersection: A New Way of Defining Records in Type Theory.
In: Proceedings of 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 22-25 June 2003, Ottawa, Canada,
LICS '03.
IEEE Computer Society,
pp. 86–95,
doi:10.1109/LICS.2003.1210048.
Joachim Lambek (1968):
A Fixpoint Theorem for Complete Categories.
Mathematische Zeitschrift 103(2),
pp. 151–161,
doi:10.1007/bf01110627.
Daniel Leivant (1989):
Contracting proofs to programs.
In: P. Odifreddi: Logic and Computer Science,
pp. 279–327,
doi:10.1184/R1/6604463.v1.
Ralph Matthes (1998):
Extensions of System F by Iteration and Primitive Recursion on Monotone Inductive Types.
Ludwig-Maximilians-Universität München.
Ralph Matthes (1998):
Monotone Fixed-Point Types and Strong Normalization.
In: Georg Gottlob, Etienne Grandjean & Katrin Seyr: Computer Science Logic, 12th International Workshop, CSL '98, Annual Conference of the EACSL, Brno, Czech Republic, August 24-28, 1998, Proceedings,
Lecture Notes in Computer Science 1584.
Springer,
pp. 298–312,
doi:10.1007/10703163_20.
Ralph Matthes (1999):
Monotone (co)inductive types and positive fixed-point types.
RAIRO - Theoretical Informatics and Applications 33(4-5),
pp. 309328,
doi:10.1051/ita:1999120.
N. P. Mendler (1987):
Recursive Types and Type Constraints in Second-Order Lambda Calculus.
In: Proceedings of the Symposium on Logic in Computer Science,
(LICS '87).
IEEE Computer Society,
Los Alamitos, CA,
pp. 30–36.
N. P. Mendler (1991):
Predictive type universes and primitive recursion.
In: Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science,
LICS '91,
pp. 173–184,
doi:10.1109/LICS.1991.151642.
Nax Paul Mendler (1991):
Inductive types and type constraints in the second-order lambda calculus.
Annals of Pure and Applied Logic 51(1),
pp. 159 – 172,
doi:10.1016/0168-0072(91)90069-X.
Alexandre Miquel (2001):
The Implicit Calculus of Constructions: Extending Pure Type Systems with an Intersection Type Binder and Subtyping.
In: Proceedings of the 5th International Conference on Typed Lambda Calculi and Applications,
TLCA01.
Springer-Verlag,
Berlin, Heidelberg,
pp. 344359,
doi:10.1007/3-540-45413-6_27.
Available at http://dl.acm.org/citation.cfm?id=1754621.1754650.
Michel Parigot (1988):
Programming with Proofs: A Second Order Type Theory.
In: Harald Ganzinger: ESOP '88, 2nd European Symposium on Programming, Nancy, France, March 21-24, 1988, Proceedings,
Lecture Notes in Computer Science 300.
Springer,
Berlin, Heidelberg,
pp. 145–159,
doi:10.1007/3-540-19027-9_10.
Michel Parigot (1989):
On the Representation of Data in Lambda-Calculus.
In: Egon Börger, Hans Kleine Büning & Michael M. Richter: CSL '89, 3rd Workshop on Computer Science Logic, Kaiserslautern, Germany, October 2-6, 1989, Proceedings,
Lecture Notes in Computer Science 440.
Springer,
Berlin, Heidelberg,
pp. 309–321,
doi:10.1007/3-540-52753-2_47.
Andrew M. Pitts (1998):
Existential Types: Logical Relations and Operational Equivalence.
In: Kim Guldstrand Larsen, Sven Skyum & Glynn Winskel: Automata, Languages and Programming, 25th International Colloquium, ICALP'98, Aalborg, Denmark, July 13-17, 1998, Proceedings,
Lecture Notes in Computer Science 1443.
Springer,
pp. 309–326,
doi:10.1007/BFb0055063.
Zdzislaw Splawski & Pawel Urzyczyn (1999):
Type Fixpoints: Iteration vs. Recursion.
In: Didier Rémy & Peter Lee: Proceedings of the fourth ACM SIGPLAN International Conference on Functional Programming (ICFP '99), Paris, France, September 27-29, 1999.
ACM,
pp. 102–113,
doi:10.1145/317636.317789.
Aaron Stump (2017):
The calculus of dependent lambda eliminations.
J. Funct. Program. 27,
pp. e14,
doi:10.1017/S0956796817000053.
Aaron Stump (2018):
From realizability to induction via dependent intersection.
Ann. Pure Appl. Logic 169(7),
pp. 637–655,
doi:10.1016/j.apal.2018.03.002.
Alfred Tarski (1955):
A lattice-theoretical fixpoint theorem and its applications.
Pacific Journal of Mathematics 5(2),
pp. 285–309,
doi:10.2140/pjm.1955.5.285.
Tarmo Uustalu & Varmo Vene (2000):
Coding Recursion a la Mendler (Extended Abstract).
In: Proc. of the 2nd Workshop on Generic Programming, WGP 2000, Technical Report UU-CS-2000-19.
Dept. of Computer Science, Utrecht University,
pp. 69–85.
Varmo Vene (2000):
Categorical programming with inductive and coinductive types.
University of Tartu.
eptcs@eptcs.org