scientific article; zbMATH DE number 1342277
From MaRDI portal
Publication:4263867
zbMath0931.03069MaRDI QIDQ4263867
Publication date: 22 September 1999
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
consistencyfinite axiomatizationMartin-Löf's type theoryMahlo cardinalstructural recursioninduction-recursioninductively defined set
Consistency and independence results (03E35) Second- and higher-order arithmetic and fragments (03F35)
Related Items (19)
Finitary higher inductive types in the groupoid model ⋮ Unnamed Item ⋮ Turing-Completeness Totally Free ⋮ Proof-Producing Reflection for HOL ⋮ Unnamed Item ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ Induction-recursion and initial algebras. ⋮ Type-theoretic approaches to ordinals ⋮ A Syntax for Higher Inductive-Inductive Types ⋮ Constructing a universe for the setoid model ⋮ How to Reason Coinductively Informally ⋮ For Finitary Induction-Induction, Induction is Enough ⋮ Dependent Types at Work ⋮ Unnamed Item ⋮ Variations on inductive-recursive definitions ⋮ Program Testing and the Meaning Explanations of Intuitionistic Type Theory ⋮ Indexed induction-recursion ⋮ Type-level Computation Using Narrowing in Ωmega ⋮ A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
This page was built for publication:
