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

dependent type theorygeneric programminginductive definitionsinductive familiesinductive-recursive definitionsinitial algebrasMartin-Löf type theorynormalization proofs

Mathematics Subject Classification ID

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

Recommendations

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

Cited in

(17)

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

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)