The following pages link to Thomas Streicher (Q165871):
Displaying 50 items.
- (Q280836) (redirect page) (← links)
- A model of type theory in simplicial sets. A brief introduction to Voevodsky's homotopy type theory (Q280837) (← links)
- The intrinsic topology of Martin-Löf universes (Q290640) (← links)
- Relating first-order set theories, toposes and categories of classes (Q386623) (← links)
- A synthetic theory of sequential domains (Q424548) (← links)
- Constructive toposes with countable sums as models of constructive set theory (Q448336) (← links)
- Relating direct and predicate transformer partial correctness semantics for an imperative probabilistic-nondeterministic language (Q541217) (← links)
- Realizability models refuting Ishihara's boundedness principle (Q714714) (← links)
- Well-foundedness in realizability (Q850808) (← links)
- A Minkowski type duality mediating between state and predicate transformer semantics for a probabilistic nondeterministic language (Q1023294) (← links)
- Specification and design of shared resource arbitration (Q1186094) (← links)
- Independence of the induction principle and the axiom of choice in the pure calculus of constructions (Q1199547) (← links)
- Induction and recursion on the partial real line with applications to Real PCF (Q1274810) (← links)
- Inductive construction of repletion (Q1306716) (← links)
- Semantics and logic of object calculi (Q1434358) (← links)
- Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice (Q1756495) (← links)
- The Michael completion of a topos spread (Q1850095) (← links)
- Models of intuitionistic set theory in subtoposes of nested realizability toposes (Q2344624) (← links)
- Completeness of continuation models for \(\lambda_\mu\)-calculus (Q2506496) (← links)
- Relative completeness for logics of functional programs (Q2915704) (← links)
- Observationally-induced algebras in domain theory (Q2921115) (← links)
- (Q3030233) (← links)
- Impredicativity entails untypedness (Q3146246) (← links)
- Domain-Theoretic Foundations of Functional Programming (Q3415205) (← links)
- Shoenfield is Gödel after Krivine (Q3437042) (← links)
- (Q3532205) (← links)
- Relating First-Order Set Theories and Elementary Toposes (Q3533518) (← links)
- Universality Results for Models in Locally Boolean Domains (Q3613357) (← links)
- (Q3634677) (← links)
- (Q3709889) (← links)
- Dependence and independence results for (impredicative) calculi of dependent types (Q4006238) (← links)
- Classical logic, continuation semantics and abstract machines (Q4240152) (← links)
- (Q4247303) (← links)
- General synthetic domain theory – a logical approach (Q4248542) (← links)
- (Q4282579) (← links)
- A universality theorem for PCF with recursive types, parallel-or and ∃ (Q4286532) (← links)
- (Q4362975) (← links)
- Partial toposes (Q4429196) (← links)
- (Q4499219) (← links)
- (Q4580318) (← links)
- A Classical Realizability Model arising from a Stable Model of Untyped Lambda Calculus (Q4596803) (← links)
- On the non-sequential nature of the interval-domain model of real-number computation (Q4659540) (← links)
- (Q4660567) (← links)
- (Q4733863) (← links)
- In Domain Realizability, not all Functionals on C[–1, 1] are Continuous (Q4787855) (← links)
- An Essential Local Geometric Morphism which is not Locally Connected though its Inverse Image Part defines an Exponential Ideal (Q5006461) (← links)
- Categorical reconstruction of a reduction free normalization proof (Q5057474) (← links)
- The genesis of the groupoid model (Q5084310) (← links)
- Triposes as a generalization of localic geometric morphisms (Q5084312) (← links)
- Independence results for calculi of dependent types (Q5096258) (← links)
