{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T09:55:18Z","timestamp":1648893318425},"reference-count":15,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":5323,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[1999]]},"DOI":"10.1016\/s1571-0661(04)00101-x","type":"journal-article","created":{"date-parts":[[2004,2,5]],"date-time":"2004-02-05T10:34:35Z","timestamp":1075977275000},"page":"13-26","source":"Crossref","is-referenced-by-count":7,"title":["Local Realizability Toposes and a Modal Logic for Computability"],"prefix":"10.1016","volume":"23","author":[{"given":"Steven","family":"Awodey","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dana S.","family":"Scott","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)00101-X_NEWBIB1","doi-asserted-by":"crossref","unstructured":"ZE-L. Benaissa, E. Moggi, W. Taha, and T. Sheard. A categorical analysis of multi-level languages. Manuscript, January 1999.","DOI":"10.1007\/3-540-49099-X_13"},{"key":"10.1016\/S1571-0661(04)00101-X_NEWBIB2","doi-asserted-by":"crossref","unstructured":"P.N. Benton. A mixed linear and non-linear logic: Proofs, terms and models (preliminary report). Technical report, University of Cambridge, 1995.","DOI":"10.1007\/BFb0022251"},{"key":"10.1016\/S1571-0661(04)00101-X_NEWBIB3","unstructured":"L. Birkedal. Developing theories of types of computability. Thesis Proposal, April 1998."},{"key":"10.1016\/S1571-0661(04)00101-X_NEWBIB4","series-title":"Applications of Sheaves","first-page":"302","article-title":"Sheaves and logic","author":"Fourman","year":"1979"},{"key":"10.1016\/S1571-0661(04)00101-X_NEWBIB5","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1017\/S0305004100057534","article-title":"Tripos theory","volume":"88","author":"Hyland","year":"1980","journal-title":"Math. Proc. Camb. Phil. Soc"},{"key":"10.1016\/S1571-0661(04)00101-X_NEWBIB6","unstructured":"P.T. Johnstone. Topos Theory. Number 10 in LMS Mathematical Monographs. Academic Press, London, 1977."},{"issue":"58","key":"10.1016\/S1571-0661(04)00101-X_NEWBIB7","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1112\/plms\/s3-58.2.281","article-title":"Local maps of toposes","volume":"3","author":"Johnstone","year":"1989","journal-title":"Proc. London Math. Soc"},{"issue":"2","key":"10.1016\/S1571-0661(04)00101-X_NEWBIB8","first-page":"289","article-title":"On the complete lattice of essential localizations","volume":"XLI","author":"Kelly","year":"1989","journal-title":"Bull. Soc. Math. Belg. Ser. A"},{"key":"10.1016\/S1571-0661(04)00101-X_NEWBIB9","unstructured":"F.W. Lawvere. Toposes generated by codiscrete objects in combinatorial topology and functional analysis. Notes for Colloquium lectures given at North Ryde, New South Wales, Australia on April 18, 1989 and at Madison, USA, on December 1, 1989, 1989."},{"key":"10.1016\/S1571-0661(04)00101-X_NEWBIB10","doi-asserted-by":"crossref","unstructured":"F.W. Lawvere. Some thoughts on the future of category theory. In A. Carboni, M.C. Pedicchio, and G. Rosolini, editors, Category Theory. Proceedings of the International conference held in Como, Italy, July 22-28, 1990, volume1488 of Lecture Notes in Mathematics, pages 1013. Springer-Verlag, 1991.","DOI":"10.1007\/BFb0084208"},{"key":"10.1016\/S1571-0661(04)00101-X_NEWBIB11","unstructured":"J. Longley. The sequentially realizable functionals. Technical Report ECS-LFCS-98-402, University of Edinburgh, 1988."},{"key":"10.1016\/S1571-0661(04)00101-X_NEWBIB12","unstructured":"J. van Oosten. A combinatory algebra for sequential functionals of finite type. Technical Report 996, University of Utrecht, 1997."},{"key":"10.1016\/S1571-0661(04)00101-X_NEWBIB13","unstructured":"A.M. Pitts. The Theory of Triposes. PhD thesis, Cambridge University, 1981."},{"key":"10.1016\/S1571-0661(04)00101-X_NEWBIB14","series-title":"Computability in Analysis and Physics","author":"Pour-El","year":"1989"},{"key":"10.1016\/S1571-0661(04)00101-X_NEWBIB15","unstructured":"D.S. Scott, S. Awodey, A. Bauer, L. Birkedal, and J. Hughes. Logics of Types and Computation at Carnegie Mellon University. http:\/\/www.cs.cmu.edu.\/Groups\/LTC\/."}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S157106610400101X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S157106610400101X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,3,30]],"date-time":"2020-03-30T12:31:29Z","timestamp":1585571489000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S157106610400101X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"references-count":15,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1999]]}},"alternative-id":["S157106610400101X"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)00101-x","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[1999]]}}}