A constructive manifestation of the Kleene-Kreisel continuous functionals (Q290639): Difference between revisions

@@ Property / author @@
+Martín Hötzel Escardó
@@ Property / author: Martín Hötzel Escardó / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Agda
@@ Property / describes a project that uses: Agda / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1016/j.apal.2016.04.011
+Normal rank
@@ Property / OpenAlex ID @@
+W2341132922
@@ Property / OpenAlex ID: W2341132922 / rank @@
+Normal rank
@@ Property / cites work @@
+Convenient categories of smooth spaces
@@ Property / cites work: Convenient categories of smooth spaces / rank @@
+Normal rank
@@ Property / cites work @@
+Compactly generated domain theory
@@ Property / cites work: Compactly generated domain theory / rank @@
+Normal rank
@@ Property / cites work @@
+Equilogical spaces
@@ Property / cites work: Equilogical spaces / rank @@
+Normal rank
@@ Property / cites work @@
+Q3803111
@@ Property / cites work: Q3803111 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5591514
@@ Property / cites work: Q5591514 / rank @@
+Normal rank
@@ Property / cites work @@
+Dependent Types at Work
@@ Property / cites work: Dependent Types at Work / rank @@
+Normal rank
@@ Property / cites work @@
+The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories
+Normal rank
@@ Property / cites work @@
+A Note on Forcing and Type Theory
@@ Property / cites work: A Note on Forcing and Type Theory / rank @@
+Normal rank
@@ Property / cites work @@
+A Computational Interpretation of Forcing in Type Theory
+Normal rank
@@ Property / cites work @@
+Q3142163
@@ Property / cites work: Q3142163 / rank @@
+Normal rank
@@ Property / cites work @@
+Revisiting the categorical interpretation of dependent type theory
+Normal rank
@@ Property / cites work @@
+Internal type theory
@@ Property / cites work: Internal type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Comparing Cartesian closed categories of (core) compactly generated spaces
+Normal rank
@@ Property / cites work @@
+The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation
+Normal rank
@@ Property / cites work @@
+Q3335779
@@ Property / cites work: Q3335779 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3693527
@@ Property / cites work: Q3693527 / rank @@
+Normal rank
@@ Property / cites work @@
+Continuous Truth II: Reflections
@@ Property / cites work: Continuous Truth II: Reflections / rank @@
+Normal rank
@@ Property / cites work @@
+Q4474857
@@ Property / cites work: Q4474857 / rank @@
+Normal rank
@@ Property / cites work @@
+Filter spaces and continuous functionals
@@ Property / cites work: Filter spaces and continuous functionals / rank @@
+Normal rank
@@ Property / cites work @@
+Q3671978
@@ Property / cites work: Q3671978 / rank @@
+Normal rank
@@ Property / cites work @@
+On a Topological Topos
@@ Property / cites work: On a Topological Topos / rank @@
+Normal rank
@@ Property / cites work @@
+Q4783274
@@ Property / cites work: Q4783274 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4040149
@@ Property / cites work: Q4040149 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5316371
@@ Property / cites work: Q5316371 / rank @@
+Normal rank
@@ Property / cites work @@
+On the ubiquity of certain total type structures
@@ Property / cites work: On the ubiquity of certain total type structures / rank @@
+Normal rank
@@ Property / cites work @@
+Higher-Order Computability
@@ Property / cites work: Higher-Order Computability / rank @@
+Normal rank
@@ Property / cites work @@
+Sheaves in geometry and logic: a first introduction to topos theory
+Normal rank
@@ Property / cites work @@
+Q3688389
@@ Property / cites work: Q3688389 / rank @@
+Normal rank
@@ Property / cites work @@
+Dependently Typed Programming in Agda
@@ Property / cites work: Dependently Typed Programming in Agda / rank @@
+Normal rank
@@ Property / cites work @@
+Recursion on the countable functionals
@@ Property / cites work: Recursion on the countable functionals / rank @@
+Normal rank
@@ Property / cites work @@
+Computing with Functionals—Computability Theory or Computer Science?
+Normal rank
@@ Property / cites work @@
+Locally cartesian closed categories and type theory
+Normal rank
@@ Property / cites work @@
+Quasi-topologies
@@ Property / cites work: Quasi-topologies / rank @@
+Normal rank
@@ Property / cites work @@
+Homotopy Type Theory: Univalent Foundations of Mathematics
+Normal rank
@@ Property / cites work @@
+Sheaf models for choice sequences
@@ Property / cites work: Sheaf models for choice sequences / rank @@
+Normal rank
@@ Property / cites work @@
+A Constructive Model of Uniform Continuity
@@ Property / cites work: A Constructive Model of Uniform Continuity / rank @@
+Normal rank