Induction-recursion and initial algebras.

DOI10.1016/S0168-0072(02)00096-9MaRDI QIDQ1412830zbMATH OpenOpenAlexFDO

Authors Peter Dybjer, Anton Setzer

Publication date 25 November 2003

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s0168-0072(02)00096-9

zbMATH Keywords

[https://portal.mardi4nfdi.de/w/index.php?title=+Special%3ASearch&search=Martin-L%EF%BF%BD%EF%BF%BDf+type+theory&go=Go Martin-L��f type theory]initial algebrasconstructive type theorydependent type theoryinductive definitionMahlo cardinalsslice categoriesinductive-recursive definitions

Mathematics Subject Classification ID

Logic in computer science (03B70) Metamathematics of constructive systems (03F50) Categorical semantics of formal languages (18C50) Abstract data types; algebraic specification (68Q65) Large cardinals (03E55) Second- and higher-order arithmetic and fragments (03F35)

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)