scientific article; zbMATH DE number 1302061

zbMath0931.03070MaRDI QIDQ4247306

Per Martin-Löf

Publication date: 21 February 2000

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

zbMATH Keywords

normalizationtranslationsintuitionistic logicintuitionistic type theorypredicativityGirard's paradox

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50) Subsystems of classical logic (including intuitionistic logic) (03B20) Intuitionistic mathematics (03F55)

Related Items (39)

Unnamed Item ⋮ The intrinsic topology of Martin-Löf universes ⋮ Proof-relevance in Bishop-style constructive mathematics ⋮ Cubical methods in homotopy type theory and univalent foundations ⋮ Generalized algebraic theories and contextual categories ⋮ From realizability to induction via dependent intersection ⋮ Direct spectra of Bishop spaces and their limits ⋮ Homotopy type theory and Voevodsky’s univalent foundations ⋮ Intuitionistic completeness of first-order logic ⋮ The metatheory of UTT ⋮ Univalent Foundations and the Equivalence Principle ⋮ Models of HoTT and the Constructive View of Theories ⋮ Checking algorithms for Pure Type Systems ⋮ A modal type theory for formalizing trusted communications ⋮ Game semantics of Martin-Löf type theory ⋮ Identity and intensionality in univalent foundations and philosophy ⋮ A constructive approach to state description semantics ⋮ Compactness notions for an apartness space ⋮ THF0 – The Core of the TPTP Language for Higher-Order Logic ⋮ Differentiating convex functions constructively ⋮ From Mathesis Universalis to Provability, Computability, and Constructivity ⋮ A two-level approach towards lean proof-checking ⋮ Constructive belief reports ⋮ Cubical Type Theory: a constructive interpretation of the univalence axiom ⋮ Typing in reflective combinatory logic ⋮ A computer-verified monadic functional implementation of the integral ⋮ Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory ⋮ The harmony of identity ⋮ Computer Certified Efficient Exact Reals in Coq ⋮ Type Theory Should Eat Itself ⋮ On the strength of dependent products in the type theory of Martin-Löf ⋮ Canonicity for cubical type theory ⋮ Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems ⋮ Type Theory and Homotopy ⋮ Program Testing and the Meaning Explanations of Intuitionistic Type Theory ⋮ Coalgebras as Types Determined by Their Elimination Rules ⋮ Indexed induction-recursion ⋮ Algebras of complemented subsets ⋮ Normalization by Evaluation for Martin-Löf Type Theory with One Universe

This page was built for publication: