6 found
Sort by:
  1. Andrej Bauer, Thierry Coquand, Giovanni Sambin & Peter M. Schuster (2012). Preface. Annals of Pure and Applied Logic 163 (2):85-86.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  2. Andrej Bauer & Davorin Lešnik (2012). Metric Spaces in Synthetic Topology. Annals of Pure and Applied Logic 163 (2):87-100.
  3. Andrej Bauer & Iztok Kavkler (2009). A Constructive Theory of Continuous Domains Suitable for Implementation. 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)  
     
    My bibliography  
     
    Export citation  
  4. Steven Awodey & Andrej Bauer (2008). Sheaf Toposes for Realizability. Archive for Mathematical Logic 47 (5):465-478.
    Steve Awodey and Audrej Bauer. Sheaf Toposes for Realizability.
    No categories
    Direct download (8 more)  
     
    My bibliography  
     
    Export citation  
  5. Andrej Bauer & Alex Simpson (2004). Two Constructive Embedding‐Extension Theorems with Applications to Continuity Principles and to Banach‐Mazur Computability. 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 (...)
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  6. Steve Awodey & Andrej Bauer, Propositions as [Types].
    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)  
     
    My bibliography  
     
    Export citation