scientific article; zbMATH DE number 2006633

MaRDI QIDQ4436029zbMATH OpenFDO

Authors Peter Dybjer, Anton Setzer

Publication date 23 November 2003

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2183/21830093.htm

zbMATH Keywords

initial algebrasdependent type theoryinductive definitionsgeneric programminginductive-recursive definitionsinductive familiesMartin-Löf type theorynormalization proofs

Mathematics Subject Classification ID

Logic in computer science (03B70) Metamathematics of constructive systems (03F50) Second- and higher-order arithmetic and fragments (03F35) Inductive definability (03D70)

Recommendations

• Indexed induction-recursion
• scientific article; zbMATH DE number 1342277
• Induction-recursion and initial algebras.
• Inductive families
• Positive inductive-recursive definitions

Cited in

(16)

• Constructive membership predicates as index types
• Inductive-inductive definitions
• Theoretical Aspects of Computing - ICTAC 2004
• A general formulation of simultaneous inductive-recursive definitions in type theory
• Containers, monads and induction recursion
• Positive inductive-recursive definitions
• Turing-Completeness Totally Free
• Inductive families
• A finite axiomatisation of inductive-inductive definitions
• Indexed induction-recursion
• Index-stratified types
• Positive inductive-recursive definitions
• How to reason coinductively informally
• Induction-recursion and initial algebras.
• Indexed containers
• Type theory should eat itself

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4436029)