6 found
Sort by:
  1.  20 DLs
    Steve Awodey, Lars Birkedal & Dana Scott, Local Realizability Toposes and a Modal Logic for Computability.
    This work is a step toward the development of a logic for types and computation that includes not only the usual spaces of mathematics and constructions, but also spaces from logic and domain theory. Using realizability, we investigate a configuration of three toposes that we regard as describing a notion of relative computability. Attention is focussed on a certain local map of toposes, which we first study axiomatically, and then by deriving a modal calculus as its internal logic. The resulting (...)
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  2.  7 DLs
    Lars Birkedal (2002). A General Notion of Realizability. Bulletin of Symbolic Logic 8 (2):266-282.
    We present a general notion of realizability encompassing both standard Kleene style realizability over partial combinatory algebras and Kleene style realizability over more general structures, including all partial cartesian closed categories. We shown how the general notion of realizability can be used to get models of dependent predicate logic, thus obtaining as a corollary (the known result) that the category Equ of equilogical spaces models dependent predicate logic. Moreover, we characterize when the general notion of realizability gives rise to a (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  3.  5 DLs
    Lars Birkedal (2007). Book Reviews. [REVIEW] Studia Logica 86 (1):133-135.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  4.  4 DLs
    Steve Awodey & Lars Birkedal, Elementary Axioms for Local Maps of Toposes.
    We present a complete elementary axiomatization of local maps of toposes.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  5.  1 DLs
    Lars Birkedal & Jaap van Oosten (2002). Relative and Modified Relative Realizability. Annals of Pure and Applied Logic 118 (1-2):115-132.
    The classical forms of both modified realizability and relative realizability are naturally described in terms of the Sierpinski topos. The paper puts these two observations together and explains abstractly the existence of the geometric morphisms and logical functors connecting the various toposes at issue. This is done by advancing the theory of triposes over internal partial combinatory algebras and by employing a novel notion of elementary map.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  6.  0 DLs
    Rasmus Ejlers Møgelberg, Lars Birkedal & Giuseppe Rosolini (2008). Synthetic Domain Theory and Models of Linear Abadi & Plotkin Logic. Annals of Pure and Applied Logic 155 (2):115-133.
    Plotkin suggested using a polymorphic dual intuitionistic/linear type theory as a metalanguage for parametric polymorphism and recursion. In recent work the first two authors and R.L. Petersen have defined a notion of parametric LAPL-structure, which are models of image, in which one can reason using parametricity and, for example, solve a large class of domain equations, as suggested by Plotkin.In this paper, we show how an interpretation of a strict version of Bierman, Pitts and Russo’s language image into synthetic domain (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation