scientific article; zbMATH DE number 1302061
From MaRDI portal
Publication:4247306
This is in fact a modification and extension of the author's earlier article ``An intuitionistic theory of types: Predicative part [in: H. E. Rose and J. Sheperdson (eds.), Logic Colloquium '73 (North-Holland, Amsterdam), 73-118 (1975; Zbl 0334.02016)]. Besides the material presented in the latter, there are: (1) a detailed account of Girard's paradox; (2) statements of translations, into the theory of types, of intuitionistic predicate logic, finite-order arithmetic, and a version of analysis (the last two with axioms of choice); (3) a proof of the completeness, relative to the theory of types, of the \(\to, \forall\)-fragment of intuitionistic first-order predicate logic. For the entire collection see [Zbl 0899.00026].
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
(95)- On the strength of dependent products in the type theory of Martin-Löf
- Generalized algebraic theories and contextual categories
- An intuitionistic theory of types with assumptions of high-arity variables
- Interpreting higher computations as types with totality
- Finite sets and natural numbers in intuitionistic TT
- A constructive approach to state description semantics
- A negationless interpretation of intuitionistic theories. II
- Organizing numerical theories using axiomatic type classes
- A modern perspective on type theory. From its origins until today
- Algebras of complemented subsets
- Shallow embedding of type theory is morally correct
- The harmony of identity
- Canonicity for cubical type theory
- Information and knowledge. A constructive type-theoretical approach
- Typing in reflective combinatory logic
- Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory
- Indexed induction-recursion
- From realizability to induction via dependent intersection
- Identity and intensionality in univalent foundations and philosophy
- An intensional type theory: Motivation and cut-elimination
- Type theory should eat itself
- Type theory in type theory using quotient inductive types
- Type theory and language constructs for objects with states
- The intrinsic topology of Martin-Löf universes
- Homotopy type theory and Voevodsky's univalent foundations
- Notions of anonymous existence in Martin-Löf type theory
- Weakly Definable Types
- A minimalistic many-valued theory of types
- The Clausal Theory of Types
- From mathesis universalis to provability, computability, and constructivity
- scientific article; zbMATH DE number 3853066 (Why is no real title available?)
- scientific article; zbMATH DE number 5360215 (Why is no real title available?)
- THF0 – The Core of the TPTP Language for Higher-Order Logic
- Hoare type theory, polymorphism and separation
- Completeness and cut-elimination in the intuitionistic theory of types. II.
- Intuitionistic completeness of first-order logic
- The logic of first order intuitionistic type theory with weak sigma-elimination
- scientific article; zbMATH DE number 45491 (Why is no real title available?)
- A modal type theory for formalizing trusted communications
- An implementation of the Heine-Borel covering theorem in type theory
- scientific article; zbMATH DE number 1302060 (Why is no real title available?)
- scientific article; zbMATH DE number 733401 (Why is no real title available?)
- scientific article; zbMATH DE number 1062114 (Why is no real title available?)
- The structure of Nuprl's type theory
- Type-theoretic functional semantics
- Compactness notions for an apartness space
- Cubical type theory: a constructive interpretation of the univalence axiom
- Reflective semantics of constructive type theory
- A two-level approach towards lean proof-checking
- scientific article; zbMATH DE number 1361532 (Why is no real title available?)
- scientific article; zbMATH DE number 3997763 (Why is no real title available?)
- scientific article; zbMATH DE number 2110617 (Why is no real title available?)
- Introduction to generalized type systems
- An interpretation of the fan theorem in type theory
- Direct spectra of Bishop spaces and their limits
- Type theory with opposite types: a paraconsistent type theory
- Proof-relevance in Bishop-style constructive mathematics
- Cubical methods in homotopy type theory and univalent foundations
- scientific article; zbMATH DE number 7269245 (Why is no real title available?)
- Constructive belief reports
- Dialectica models of type theory
- Differentiating convex functions constructively
- Computer Certified Efficient Exact Reals in Coq
- Type theory and homotopy
- Program testing and the meaning explanations of intuitionistic type theory
- Coalgebras as types determined by their elimination rules
- Normalization by Evaluation for Martin-Löf Type Theory with One Universe
- Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems
- An Intuitionistic Version of Cantor's Theorem
- A partial translation from \({\lambda}U\) to \({\lambda}2\)
- Integrating classical and intuitionistic type theory
- Foundations of mathematics in polymorphic type theory
- 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
- Game semantics of Martin-Löf type theory
- Pre-measure spaces and pre-integration spaces in predicative Bishop-Cheng measure theory
- Correct and complete type checking and certified erasure for \textsc{Coq}, in \textsc{Coq}
- The paradox of trees in type theory
- On specifications, subset types and interpretation of proposition in type theory
- A constructive interpretation of the logical constants
- Comodule representations of second-order functionals
- First-order homotopical logic
- On symmetries of spheres in univalent foundations
- On the Weihrauch degree of the additive Ramsey theorem
- Hilbert's tenth problem for term algebras with a substitution operator
- Complemented subsets and Boolean-valued, partial functions
- scientific article; zbMATH DE number 7979452 (Why is no real title available?)
- Judgmental and definitional equality from a Fregean perspective
- Paradoxical connectives: proof-theoretic semantics, recursion, and fixed-point operators
- Principal type schemes for an extended type theory
- Realizability and intuitionistic logic
- The role of compactification theory in the type problem
- A computer-verified monadic functional implementation of the integral
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)
