scientific article; zbMATH DE number 1302061
From MaRDI portal
Publication:4247306
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
Cited in
(81)- Intuitionistic completeness of first-order logic
- Canonicity for cubical type theory
- Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems
- The paradox of trees in type theory
- scientific article; zbMATH DE number 1420788 (Why is no real title available?)
- scientific article; zbMATH DE number 1070622 (Why is no real title available?)
- Dialectica models of type theory
- scientific article; zbMATH DE number 1302060 (Why is no real title available?)
- Foundations of mathematics in polymorphic type theory
- Interpreting higher computations as types with totality
- scientific article; zbMATH DE number 7269245 (Why is no real title available?)
- A modal type theory for formalizing trusted communications
- scientific article; zbMATH DE number 5360215 (Why is no real title available?)
- A minimalistic many-valued theory of types
- THF0 – The Core of the TPTP Language for Higher-Order Logic
- An intensional type theory: Motivation and cut-elimination
- Completeness and cut-elimination in the intuitionistic theory of types. II.
- Type theory and homotopy
- 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
- A two-level approach towards lean proof-checking
- Generalized algebraic theories and contextual categories
- Models of HoTT and the Constructive View of Theories
- Indexed induction-recursion
- From mathesis universalis to provability, computability, and constructivity
- The metatheory of UTT
- Organizing numerical theories using axiomatic type classes
- Computer Certified Efficient Exact Reals in Coq
- Direct spectra of Bishop spaces and their limits
- Weakly Definable Types
- scientific article; zbMATH DE number 733401 (Why is no real title available?)
- Proof-relevance in Bishop-style constructive mathematics
- Typing in reflective combinatory logic
- Type theory in type theory using quotient inductive types
- The intrinsic topology of Martin-Löf universes
- Homotopy type theory and Voevodsky's univalent foundations
- scientific article; zbMATH DE number 1301730 (Why is no real title available?)
- Game semantics of Martin-Löf type theory
- Univalent Foundations and the Equivalence Principle
- A negationless interpretation of intuitionistic theories. II
- Pre-measure spaces and pre-integration spaces in predicative Bishop-Cheng measure theory
- Identity and intensionality in univalent foundations and philosophy
- scientific article; zbMATH DE number 3853066 (Why is no real title available?)
- Program testing and the meaning explanations of intuitionistic type theory
- Normalization by Evaluation for Martin-Löf Type Theory with One Universe
- Cubical methods in homotopy type theory and univalent foundations
- On the strength of dependent products in the type theory of Martin-Löf
- Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory
- Information and knowledge. A constructive type-theoretical approach
- scientific article; zbMATH DE number 2110617 (Why is no real title available?)
- Coalgebras as types determined by their elimination rules
- On specifications, subset types and interpretation of proposition in type theory
- The harmony of identity
- Checking algorithms for Pure Type Systems
- 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
- The Clausal Theory of Types
- Type theory and language constructs for objects with states
- A partial translation from \({\lambda}U\) to \({\lambda}2\)
- Algebras of complemented subsets
- Realizability and intuitionistic logic
- Cubical type theory: a constructive interpretation of the univalence axiom
- scientific article; zbMATH DE number 45491 (Why is no real title available?)
- A computer-verified monadic functional implementation of the integral
- scientific article; zbMATH DE number 1062114 (Why is no real title available?)
- Introduction to generalized type systems
- scientific article; zbMATH DE number 1927416 (Why is no real title available?)
- The role of compactification theory in the type problem
- Notions of anonymous existence in Martin-Löf type theory
- Type theory with opposite types: a paraconsistent type theory
- Type theory should eat itself
- scientific article; zbMATH DE number 1361532 (Why is no real title available?)
- scientific article; zbMATH DE number 3997763 (Why is no real title available?)
- A modern perspective on type theory. From its origins until today
- Constructive belief reports
- Hoare type theory, polymorphism and separation
- Reflective semantics of constructive type theory
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)
