scientific article; zbMATH DE number 2006633

zbMath1024.03062MaRDI QIDQ4436029

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: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

Martin-Löf type theoryinitial algebrasdependent type theoryinductive definitionsgeneric programminginductive-recursive definitionsinductive familiesnormalization proofs

Mathematics Subject Classification ID

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

Related Items

Turing-Completeness Totally Free ⋮ Induction-recursion and initial algebras. ⋮ Indexed containers ⋮ How to Reason Coinductively Informally ⋮ Type Theory Should Eat Itself ⋮ Indexed induction-recursion