scientific article; zbMATH DE number 5233467

zbMath1127.03320MaRDI QIDQ5438968

Anton Setzer

Publication date: 8 February 2008

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

proof theoryKripke-Platek set theoryMartin-Löf type theorywellfounded treesKleene's OMahlo universe, inductive-recursive definitions, generic programmingW-type

Mathematics Subject Classification ID

Second- and higher-order arithmetic and fragments (03F35) Intuitionistic mathematics (03F55)

Related Items (3)

Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory ⋮ Indexed induction-recursion ⋮ An Upper Bound for the Proof-Theoretic Strength of Martin-Löf Type Theory with W-type and One Universe

This page was built for publication: