Induction-recursion and initial algebras.
From MaRDI portal
Recommendations
- scientific article; zbMATH DE number 4099283
- Towards an algebraic theory of recursion
- Alpha-structural recursion and induction
- Theorem Proving in Higher Order Logics
- Induction, restriction and G-algebras
- scientific article; zbMATH DE number 2221041
- Publication:4946107
- Recursion, induction and well-founded orders
- An introduction to (co)algebra and (co)induction
- Recursively defined domains and their induction principles
Cites work
- scientific article; zbMATH DE number 3859117 (Why is no real title available?)
- scientific article; zbMATH DE number 3910392 (Why is no real title available?)
- scientific article; zbMATH DE number 3959364 (Why is no real title available?)
- scientific article; zbMATH DE number 3722625 (Why is no real title available?)
- scientific article; zbMATH DE number 50149 (Why is no real title available?)
- scientific article; zbMATH DE number 65535 (Why is no real title available?)
- scientific article; zbMATH DE number 3521950 (Why is no real title available?)
- scientific article; zbMATH DE number 1241699 (Why is no real title available?)
- scientific article; zbMATH DE number 1302063 (Why is no real title available?)
- scientific article; zbMATH DE number 1342277 (Why is no real title available?)
- scientific article; zbMATH DE number 510775 (Why is no real title available?)
- scientific article; zbMATH DE number 512790 (Why is no real title available?)
- scientific article; zbMATH DE number 2006633 (Why is no real title available?)
- scientific article; zbMATH DE number 946307 (Why is no real title available?)
- scientific article; zbMATH DE number 3328156 (Why is no real title available?)
- scientific article; zbMATH DE number 4189687 (Why is no real title available?)
- A general formulation of simultaneous inductive-recursive definitions in type theory
- Collapsing functions based on recursively large ordinals: A well-ordering proof for KPM
- Extending Martin-Löf type theory by one Mahlo-universe
- Generalized algebraic theories and contextual categories
- Inaccessibility in constructive set theory and type theory
- Inductive families
- Internal type theory
- Locally cartesian closed categories and type theory
- Ordinal notations based on a weakly Mahlo cardinal
- Proof-theoretic analysis of KPM
- Type-theoretic interpretation of iterated, strictly positive inductive definitions
Cited in
(24)- Coalgebras as types determined by their elimination rules
- Three extensional models of type theory
- A general formulation of simultaneous inductive-recursive definitions in type theory
- Continuous functions on final coalgebras
- Containers, monads and induction recursion
- scientific article; zbMATH DE number 2006633 (Why is no real title available?)
- Positive inductive-recursive definitions
- Interactive programming in Agda -- objects and graphical user interfaces
- Predicativity and constructive mathematics
- A finite axiomatisation of inductive-inductive definitions
- Indexed induction-recursion
- Type-theoretic interpretation of iterated, strictly positive inductive definitions
- Impredicative encodings of inductive-inductive data in Cedille
- Type-theoretic approaches to ordinals
- Positive inductive-recursive definitions
- Subtyping without reduction
- Small induction recursion
- How to reason coinductively informally
- Alpha-structural recursion and induction
- Variations on inductive-recursive definitions
- scientific article; zbMATH DE number 7407785 (Why is no real title available?)
- Theorem Proving in Higher Order Logics
- Intuitionistic fixed point logic
- An induction principle for nested datatypes in intensional type theory
This page was built for publication: Induction-recursion and initial algebras.
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1412830)