scientific article; zbMATH DE number 1302061

zbMATH Open0931.03070MaRDI QIDQ4247306FDOQ4247306

Authors: Per Martin-Löf 

Publication date: 21 February 2000

Title of this publication is not available (Why is that?)

Recommendations

• Treatise on intuitionistic type theory
• La théorie intuitionniste des types : sémantique des preuves et théorie des constructions
• Intensional models for the theory of types
• Toposes and intuitionistic theories of types
• A theory of qualified types
• An intuitionistic theory of types with assumptions of high-arity variables
• Introduction to Type Theory
• scientific article; zbMATH DE number 3521950
• Analogical type theory
• Publication:4204148

zbMATH Keywords

intuitionistic logicnormalizationintuitionistic type theorytranslationspredicativityGirard's paradox

Mathematics Subject Classification ID

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

Cited In (81)

• Title not available (Why is that?)
• Title not available (Why is that?)
• A two-level approach towards lean proof-checking
• Models of HoTT and the Constructive View of Theories
• The metatheory of UTT
• Game semantics of Martin-Löf type theory
• Univalent Foundations and the Equivalence Principle
• Pre-measure spaces and pre-integration spaces in predicative Bishop-Cheng measure theory
• Cubical methods in homotopy type theory and univalent foundations
• Title not available (Why is that?)
• The Clausal Theory of Types
• A partial translation from \({\lambda}U\) to \({\lambda}2\)
• Reflective semantics of constructive type theory
• Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems
• Intuitionistic completeness of first-order logic
• Canonicity for cubical type theory
• The paradox of trees in type theory
• Title not available (Why is that?)
• Dialectica models of type theory
• Foundations of mathematics in polymorphic type theory
• Title not available (Why is that?)
• Interpreting higher computations as types with totality
• A modal type theory for formalizing trusted communications
• Title not available (Why is that?)
• A minimalistic many-valued theory of types
• THF0 – The Core of the TPTP Language for Higher-Order Logic
• Type theory and homotopy
• Completeness and cut-elimination in the intuitionistic theory of types. II.
• An intensional type theory: Motivation and cut-elimination
• Principal type schemes for an extended type theory
• Integrating classical and intuitionistic type theory
• Compactness notions for an apartness space
• From realizability to induction via dependent intersection
• Differentiating convex functions constructively
• Generalized algebraic theories and contextual categories
• Indexed induction-recursion
• From mathesis universalis to provability, computability, and constructivity
• Computer Certified Efficient Exact Reals in Coq
• Organizing numerical theories using axiomatic type classes
• Direct spectra of Bishop spaces and their limits
• Title not available (Why is that?)
• Proof-relevance in Bishop-style constructive mathematics
• Weakly Definable Types
• Typing in reflective combinatory logic
• Type theory in type theory using quotient inductive types
• Title not available (Why is that?)
• Homotopy type theory and Voevodsky's univalent foundations
• The intrinsic topology of Martin-Löf universes
• A negationless interpretation of intuitionistic theories. II
• Identity and intensionality in univalent foundations and philosophy
• Program testing and the meaning explanations of intuitionistic type theory
• Title not available (Why is that?)
• Normalization by Evaluation for Martin-Löf Type Theory with One Universe
• Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory
• On the strength of dependent products in the type theory of Martin-Löf
• Information and knowledge. A constructive type-theoretical approach
• Coalgebras as types determined by their elimination rules
• Checking algorithms for Pure Type Systems
• The harmony of identity
• On specifications, subset types and interpretation of proposition in type theory
• Shallow embedding of type theory is morally correct
• An intuitionistic theory of types with assumptions of high-arity variables
• A constructive approach to state description semantics
• Type theory and language constructs for objects with states
• Cubical type theory: a constructive interpretation of the univalence axiom
• Title not available (Why is that?)
• Algebras of complemented subsets
• Realizability and intuitionistic logic
• Introduction to generalized type systems
• Title not available (Why is that?)
• Title not available (Why is that?)
• A computer-verified monadic functional implementation of the integral
• Notions of anonymous existence in Martin-Löf type theory
• Type theory with opposite types: a paraconsistent type theory
• The role of compactification theory in the type problem
• Type theory should eat itself
• Title not available (Why is that?)
• Title not available (Why is that?)
• A modern perspective on type theory. From its origins until today
• Constructive belief reports
• Hoare type theory, polymorphism and separation

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 Q4247306)