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
Link To Document :
بازگشت