scientific article; zbMATH DE number 2006633

zbMATH Open1024.03062MaRDI QIDQ4436029FDOQ4436029

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

Title of this publication is not available (Why is that?)

Recommendations

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

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)

Cited In (16)

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

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)