{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,14]],"date-time":"2026-05-14T11:17:19Z","timestamp":1778757439379,"version":"3.51.4"},"reference-count":29,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2014,1,15]],"date-time":"2014-01-15T00:00:00Z","timestamp":1389744000000},"content-version":"unspecified","delay-in-days":4246,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Bull. symb. log."],"published-print":{"date-parts":[[2002,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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 <jats:bold>Equ<\/jats:bold> of equilogical spaces models dependent predicate logic. Moreover, we characterize when the general notion of realizability gives rise to a topos, <jats:italic>i.e.<\/jats:italic>, a model of impredicative intuitionistic higher-order logic.<\/jats:p>","DOI":"10.2178\/bsl\/1182353873","type":"journal-article","created":{"date-parts":[[2008,4,3]],"date-time":"2008-04-03T17:09:38Z","timestamp":1207242578000},"page":"266-282","source":"Crossref","is-referenced-by-count":1,"title":["A General Notion of Realizability"],"prefix":"10.1017","volume":"8","author":[{"given":"Lars","family":"Birkedal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,1,15]]},"reference":[{"key":"S1079898600005060_ref028","doi-asserted-by":"crossref","unstructured":"Troelstra A. S. , Handbook of Proof Theory, Studies in Logic and the Foundations of Mathematics, vol. 137, ch. VI: Realizability, pp. 407\u2013473, Studies in Logic and the Foundations of Mathematics, Elsevier Science B.V, 1998, pp. 407\u2013473.","DOI":"10.1016\/S0049-237X(98)80021-9"},{"key":"S1079898600005060_ref027","volume-title":"Cambridge studies in advanced mathematics","author":"Taylor","year":"1999"},{"key":"S1079898600005060_ref025","unstructured":"Rosolini G. , Continuity and effectiveness in Topoi, Ph.D. thesis , University of Oxford, 1986."},{"key":"S1079898600005060_ref019","volume-title":"Workshop on realizability semantics and applications","volume":"23","author":"Longley","year":"1999"},{"key":"S1079898600005060_ref022","volume-title":"Tutorial workshop on realizability semantics, FLoC'99","volume":"23","author":"Pitts","year":"1999"},{"key":"S1079898600005060_ref020","volume-title":"Sheaves in geometry and logic. A first introduction to topos theory","author":"Lane","year":"1992"},{"key":"S1079898600005060_ref023","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90034-X"},{"key":"S1079898600005060_ref026","first-page":"403","volume-title":"To H. B. Curry: Essays in combinatory logic","author":"Scott","year":"1980"},{"key":"S1079898600005060_ref010","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-67678-9"},{"key":"S1079898600005060_ref018","unstructured":"Longley J. , Unifying typed and untyped realizability, Available at http:\/\/www.dcs.ed.ac.uk\/home\/jrl\/unifying.txt, 05 1999."},{"key":"S1079898600005060_ref007","article-title":"Locally cartesian closed exact completions","author":"Carboni","year":"1999","journal-title":"Journal of Pure and Applied Algebra"},{"key":"S1079898600005060_ref013","volume-title":"Studies in logic and the foundations of mathematics","volume":"141","author":"Jacobs","year":"1999"},{"key":"S1079898600005060_ref001","first-page":"27","article-title":"Equilogical spaces","author":"Bauer","year":"1998","journal-title":"TCS"},{"key":"S1079898600005060_ref003","volume-title":"Proceedings of the 15th annual IEEE symposium on logic in computer science","author":"Birkedal","year":"2000"},{"key":"S1079898600005060_ref017","volume-title":"Mathematical Structures in Computer Science","author":"Lietz","year":"2000"},{"key":"S1079898600005060_ref004","first-page":"188","volume-title":"Proceedings of the 13th annual IEEE symposium on logic in computer science","author":"Birkedal","year":"1998"},{"key":"S1079898600005060_ref009","unstructured":"de Marchi F. , Robinson E. P. , and Rosolini G. , An abstract look at realizability, Working Draft, 11 27, 1999."},{"key":"S1079898600005060_ref015","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0066772"},{"key":"S1079898600005060_ref021","unstructured":"Pitts A. M. , The theory of triposes, Ph.D. thesis , University of Cambridge, 1981."},{"key":"S1079898600005060_ref005","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(94)00103-P"},{"key":"S1079898600005060_ref006","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-19020-1_2"},{"key":"S1079898600005060_ref024","doi-asserted-by":"publisher","DOI":"10.2307\/2274658"},{"key":"S1079898600005060_ref011","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(09)70129-6"},{"key":"S1079898600005060_ref002","doi-asserted-by":"crossref","unstructured":"Birkedal L. , Developing theories of types and computability via realizability, Electronic notes in theoretical computer science, vol. 34, 2000, Book version of PhD-thesis, pp. viii + 282.","DOI":"10.1016\/S1571-0661(05)80642-5"},{"key":"S1079898600005060_ref012","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100057534"},{"key":"S1079898600005060_ref014","doi-asserted-by":"publisher","DOI":"10.2307\/2269016"},{"key":"S1079898600005060_ref029","volume-title":"Tutorial workshop on realizability semantics, FLoC'99","volume":"23","author":"van Oosten","year":"1999"},{"key":"S1079898600005060_ref016","volume-title":"Introduction to higher order categorical logic","author":"Lambek","year":"1986"},{"key":"S1079898600005060_ref008","volume-title":"Introduction to lattices and order","author":"Davey","year":"1990"}],"container-title":["Bulletin of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1079898600005060","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,7]],"date-time":"2019-05-07T01:04:25Z","timestamp":1557191065000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1079898600005060\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,6]]},"references-count":29,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2002,6]]}},"alternative-id":["S1079898600005060"],"URL":"https:\/\/doi.org\/10.2178\/bsl\/1182353873","relation":{},"ISSN":["1079-8986","1943-5894"],"issn-type":[{"value":"1079-8986","type":"print"},{"value":"1943-5894","type":"electronic"}],"subject":[],"published":{"date-parts":[[2002,6]]}}}