Order:
  1.  16
    Metric Spaces in Synthetic Topology.Andrej Bauer & Davorin Lešnik - 2012 - Annals of Pure and Applied Logic 163 (2):87-100.
  2.  12
    Two Constructive Embedding‐Extension Theorems with Applications to Continuity Principles and to Banach‐Mazur Computability.Andrej Bauer & Alex Simpson - 2004 - Mathematical Logic Quarterly 50 (4‐5):351-369.
    We prove two embedding and extension theorems in the context of the constructive theory of metric spaces. The first states that Cantor space embeds in any inhabited complete separable metric space without isolated points, X, in such a way that every sequentially continuous function from Cantor space to ℤ extends to a sequentially continuous function from X to ℝ. The second asserts an analogous property for Baire space relative to any inhabited locally non-compact CSM. Both results rely on having careful (...)
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  3.  22
    Sheaf Toposes for Realizability.Steven Awodey & Andrej Bauer - 2008 - Archive for Mathematical Logic 47 (5):465-478.
    Steve Awodey and Audrej Bauer. Sheaf Toposes for Realizability.
    Direct download (8 more)  
     
    Export citation  
     
    My bibliography  
  4. Two Constructive Embedding-Extension Theorems with Applications to Continuity Principles and to Banach-Mazur Computability.Andrej Bauer & Alex Simpson - 2004 - Mathematical Logic Quarterly 50 (45):351-369.
    We prove two embedding and extension theorems in the context of the constructive theory of metric spaces. The first states that Cantor space embeds in any inhabited complete separable metric space without isolated points, X, in such a way that every sequentially continuous function from Cantor space to ℤ extends to a sequentially continuous function from X to ℝ. The second asserts an analogous property for Baire space relative to any inhabited locally non-compact CSM. Both results rely on having careful (...)
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  5.  13
    Propositions as [Types].Steve Awodey & Andrej Bauer - unknown
    Image factorizations in regular categories are stable under pullbacks, so they model a natural modal operator in dependent type theory. This unary type constructor [A] has turned up previously in a syntactic form as a way of erasing computational content, and formalizing a notion of proof irrelevance. Indeed, semantically, the notion of a support is sometimes used as surrogate proposition asserting inhabitation of an indexed family. We give rules for bracket types in dependent type theory and provide complete semantics using (...)
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  6.  2
    A Constructive Theory of Continuous Domains Suitable for Implementation.Andrej Bauer & Iztok Kavkler - 2009 - Annals of Pure and Applied Logic 159 (3):251-267.
    We formulate a predicative, constructive theory of continuous domains whose realizability interpretation gives a practical implementation of continuous ω-chain complete posets and continuous maps between them. We apply the theory to implementation of the interval domain and exact real numbers.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  7.  2
    Preface.Andrej Bauer, Thierry Coquand, Giovanni Sambin & Peter M. Schuster - 2012 - Annals of Pure and Applied Logic 163 (2):85-86.