scientific article; zbMATH DE number 1302061
From MaRDI portal
Publication:4247306
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
intuitionistic logicnormalizationintuitionistic type theorytranslationspredicativityGirard's paradox
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)