• DocumentCode
    2221485
  • Title

    A general notion of realizability

  • Author

    Birkedal, L.

  • Author_Institution
    IT Univ. of Copenhagen, Denmark
  • fYear
    2000
  • fDate
    2000
  • Firstpage
    7
  • Lastpage
    17
  • Abstract
    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 show 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 topos
  • Keywords
    category theory; combinatorial mathematics; formal logic; type theory; Equ; dependent predicate logic modelling; equilogical spaces; general structures; partial cartesian closed categories; partial combinatory algebras; standard Kleene style realizability; topos; Algebra; Assembly; Electrical capacitance tomography; Lattices; Logic; Principal component analysis;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Logic in Computer Science, 2000. Proceedings. 15th Annual IEEE Symposium on
  • Conference_Location
    Santa Barbara, CA
  • ISSN
    1043-6871
  • Print_ISBN
    0-7695-0725-5
  • Type

    conf

  • DOI
    10.1109/LICS.2000.855751
  • Filename
    855751