The following pages link to (Q4247306):
Displaying 50 items.
- The intrinsic topology of Martin-Löf universes (Q290640) (← links)
- Intuitionistic completeness of first-order logic (Q392280) (← links)
- A modal type theory for formalizing trusted communications (Q420842) (← links)
- Compactness notions for an apartness space (Q453202) (← links)
- Constructive belief reports (Q514084) (← links)
- Integrating classical and intuitionistic type theory (Q580341) (← links)
- The paradox of trees in type theory (Q688725) (← links)
- On specifications, subset types and interpretation of proposition in type theory (Q688736) (← links)
- Principal type schemes for an extended type theory (Q790801) (← links)
- Realizability and intuitionistic logic (Q792319) (← links)
- The role of compactification theory in the type problem (Q934308) (← links)
- A computer-verified monadic functional implementation of the integral (Q987984) (← links)
- On the strength of dependent products in the type theory of Martin-Löf (Q1024547) (← links)
- Generalized algebraic theories and contextual categories (Q1096716) (← links)
- An intuitionistic theory of types with assumptions of high-arity variables (Q1192333) (← links)
- Interpreting higher computations as types with totality (Q1337495) (← links)
- Finite sets and natural numbers in intuitionistic TT (Q1374211) (← links)
- A constructive approach to state description semantics (Q1414570) (← links)
- A negationless interpretation of intuitionistic theories. II (Q1582305) (← links)
- Organizing numerical theories using axiomatic type classes (Q1774558) (← links)
- A modern perspective on type theory. From its origins until today (Q1887432) (← links)
- Algebras of complemented subsets (Q2104273) (← links)
- Shallow embedding of type theory is morally correct (Q2176685) (← links)
- The harmony of identity (Q2281316) (← links)
- Canonicity for cubical type theory (Q2319982) (← links)
- Information and knowledge. A constructive type-theoretical approach (Q2464131) (← links)
- Typing in reflective combinatory logic (Q2498910) (← links)
- Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory (Q2503336) (← links)
- Indexed induction-recursion (Q2577476) (← links)
- From realizability to induction via dependent intersection (Q2636522) (← links)
- Identity and intensionality in univalent foundations and philosophy (Q2695034) (← links)
- An intensional type theory: Motivation and cut-elimination (Q2732287) (← links)
- Type theory should eat itself (Q2804938) (← links)
- Type theory in type theory using quotient inductive types (Q2828239) (← links)
- Type theory and language constructs for objects with states (Q2851715) (← links)
- Homotopy type theory and Voevodsky’s univalent foundations (Q2933829) (← links)
- Notions of anonymous existence in Martin-Löf type theory (Q2980980) (← links)
- Weakly Definable Types (Q3028989) (← links)
- A minimalistic many-valued theory of types (Q3133165) (← links)
- The Clausal Theory of Types (Q3184628) (← links)
- From Mathesis Universalis to Provability, Computability, and Constructivity (Q3305633) (← links)
- (Q3532203) (← links)
- THF0 – The Core of the TPTP Language for Higher-Order Logic (Q3541725) (← links)
- Hoare type theory, polymorphism and separation (Q3546051) (← links)
- Completeness and Cut-elimination in the Intuitionistic Theory of Types--Part 2 (Q3553922) (← links)
- The logic of first order intuitionistic type theory with weak sigma-elimination (Q3984424) (← links)
- (Q3995928) (← links)
- (Q4246943) (← links)
- (Q4247305) (← links)
- (Q4354787) (← links)
