Induction–recursion and initial algebras
Authors:
- Peter DybjerPDPeter Dybjer
- Anton SetzerASAnton Setzer
- 1 December 2003
- journal article
- Published by Elsevier in Annals of Pure and Applied Logic
- Vol. 124 (1-3) , 1-47
Abstract
No abstract availableKeywords
This publication has 16 references indexed in Scilit:
- Inductive definitions in the system Coq rules and properties2005
- A general formulation of simultaneous inductive-recursive definitions in type theoryThe Journal of Symbolic Logic, 2000
- Inaccessibility in constructive set theory and type theoryAnnals of Pure and Applied Logic, 1998
- Inductive familiesFormal Aspects of Computing, 1994
- Collapsing functions based on recursively large ordinals: A well-ordering proof for KPMArchive for Mathematical Logic, 1994
- Type-theoretic interpretation of iterated, strictly positive inductive definitionsArchive for Mathematical Logic, 1992
- Ordinal notations based on a weakly Mahlo cardinalArchive for Mathematical Logic, 1990
- Generalised algebraic theories and contextual categoriesAnnals of Pure and Applied Logic, 1986
- Locally cartesian closed categories and type theoryMathematical Proceedings of the Cambridge Philosophical Society, 1984
- Constructive validity1970