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
initial algebrasdependent type theoryinductive definitionsgeneric programminginductive-recursive definitionsinductive familiesMartin-Löf type theorynormalization proofs
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)