{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T22:46:57Z","timestamp":1649198817759},"reference-count":32,"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)00106-9","type":"journal-article","created":{"date-parts":[[2004,2,5]],"date-time":"2004-02-05T10:34:35Z","timestamp":1075977275000},"page":"101-110","source":"Crossref","is-referenced-by-count":1,"title":["History and Developments"],"prefix":"10.1016","volume":"23","author":[{"given":"Jaap","family":"van Oosten","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)00106-9_NEWBIB1","unstructured":"P.H.G. Aczel. A note on interpreting intuitionistic hiher-order logic, 1980. Handwritten note."},{"key":"10.1016\/S1571-0661(04)00106-9_NEWBIB2","doi-asserted-by":"crossref","unstructured":"S. Awodey, L. Birkedal, and D.S. Scott. Local realizability toposes and a modal logic for computability. Presented at Tutorial Workshop on Realizability Semantics, FLoC'99, trento, Italy 1999., 1999.","DOI":"10.1016\/S1571-0661(04)00101-X"},{"key":"10.1016\/S1571-0661(04)00106-9_NEWBIB3","unstructured":"D.H.J. de Jongh. The maximality of the intuitionistic predicate calculus with respect to Heything's Arithmetic, 1969. Typed manuscript from University of Wisconsin, Madison."},{"key":"10.1016\/S1571-0661(04)00106-9_NEWBIB4","series-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","first-page":"491","article-title":"Modified realization and the formulac-as-types notion","author":"Diller","year":"1980"},{"key":"10.1016\/S1571-0661(04)00106-9_NEWBIB5","first-page":"458","article-title":"Transfinite completions of constructive arithmetical calculus (Russian)","volume":"189","author":"Dragalin","year":"1969","journal-title":"Doklady"},{"key":"10.1016\/S1571-0661(04)00106-9_NEWBIB6","series-title":"Algebra and Logic","first-page":"87","article-title":"A language and axioms for explicit mathematics","author":"Feferman","year":"1975"},{"key":"10.1016\/S1571-0661(04)00106-9_NEWBIB7","first-page":"18","article-title":"Recursive realizability from the intuitionistic point of view (Russian)","volume":"256","author":"Gavrilenko","year":"1981","journal-title":"Doklady"},{"key":"10.1016\/S1571-0661(04)00106-9_NEWBIB8","first-page":"34","article-title":"Zur intuitionistischen arithmetic und zahlentheorie","volume":"4","author":"G\u00f6del","year":"1932","journal-title":"Ergebnisse eines mathematisches Kolloquiums"},{"key":"10.1016\/S1571-0661(04)00106-9_NEWBIB9","doi-asserted-by":"crossref","first-page":"23","DOI":"10.2307\/2271946","article-title":"Relativized realizability in intuitionistic arithmetic of all finite types","volume":"43","author":"Goodman","year":"1978","journal-title":"Jouirnal of Symbolic Logic"},{"key":"10.1016\/S1571-0661(04)00106-9_NEWBIB10","series-title":"Grundlagen der Mathematik I","author":"Hilbert","year":"1934"},{"key":"10.1016\/S1571-0661(04)00106-9_NEWBIB11","series-title":"Essays on Combinatory Logic, Lambda Calculus, and Formalism","article-title":"To H.B. Curry: The formulae-as-types notion of construction","author":"Howard","year":"1969"},{"key":"10.1016\/S1571-0661(04)00106-9_NEWBIB12","doi-asserted-by":"crossref","unstructured":"J.M.E. Hyland, and C.-H. L. Ong. Modified realizability toposes and strong normalization proofs. In J.F. Groote and M. Bezem, editors, Typed Lambda Calculi and Applications, volume 664 of Lectrue Notes in Computer Science, pages 179\u2013194. Springer-Verlag, 1993.","DOI":"10.1007\/BFb0037106"},{"key":"10.1016\/S1571-0661(04)00106-9_NEWBIB13","doi-asserted-by":"crossref","first-page":"109","DOI":"10.2307\/2269016","article-title":"On the interpretation of intuitionistic number theory","volume":"10","author":"Kleene","year":"1945","journal-title":"Journal of Symjbolic Logic"},{"key":"10.1016\/S1571-0661(04)00106-9_NEWBIB14","series-title":"Introduction to metamathemaitics","author":"Kleene","year":"1980"},{"key":"10.1016\/S1571-0661(04)00106-9_NEWBIB15","first-page":"71","article-title":"Logical calculus and realizability","volume":"18","author":"Kleene","year":"1965","journal-title":"Acta Philosophica Fennica"},{"key":"10.1016\/S1571-0661(04)00106-9_NEWBIB16","doi-asserted-by":"crossref","unstructured":"S.C. Kleene. Formalized Recursive Functionals and Formalized Relizability, volume 89 of Memoirs of the American Mathematical Society. American Mathematical Society, 1969.","DOI":"10.1090\/memo\/0089"},{"key":"10.1016\/S1571-0661(04)00106-9_NEWBIB17","doi-asserted-by":"crossref","unstructured":"S.C. Kleene. Realizability: a retrospective survey. In A.R.D. Mathias and H. Rogers editors, Cambridge Summer Summer School in Mathematical logic, volume 337 of LETURE Notes in Mathematics, pages 95\u2013112. Springer-Verlag, 1973.","DOI":"10.1007\/BFb0066772"},{"key":"10.1016\/S1571-0661(04)00106-9_NEWBIB18","series-title":"The Foundations of Intuitionistic Mathematics, especially in relation to recursive functions","author":"Kleene","year":"1965"},{"key":"10.1016\/S1571-0661(04)00106-9_NEWBIB19","series-title":"Constructivity in mathematics","first-page":"101","article-title":"Interpretation of analyusis by means of functioals of finite type","author":"Kreisel","year":"1959"},{"key":"10.1016\/S1571-0661(04)00106-9_NEWBIB20","first-page":"1015","article-title":"Finite problems (Russian)","volume":"142","author":"Medvedev","year":"1962","journal-title":"Doklady"},{"key":"10.1016\/S1571-0661(04)00106-9_NEWBIB21","doi-asserted-by":"crossref","first-page":"309","DOI":"10.2307\/2270266","article-title":"Can there be no nonrecursive funmctions?","volume":"36","author":"Moschovakis","year":"1971","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1571-0661(04)00106-9_NEWBIB22","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1090\/S0002-9947-1947-0025420-1","article-title":"Recursive functions and intuitionistic number theory","volume":"61","author":"Nelson","year":"1947","journal-title":"Transactions of the American Mathematical Society"},{"key":"10.1016\/S1571-0661(04)00106-9_NEWBIB23","first-page":"315","article-title":"Absolute realizability of predicate formulas (Russian)","volume":"47","author":"Plisko","year":"1983","journal-title":"Izv. Akad. Nauk"},{"key":"10.1016\/S1571-0661(04)00106-9_NEWBIB24","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1090\/S0002-9947-1953-0055952-4","article-title":"Propositional caculus and realizinility","volume":"75","author":"Rose","year":"1953","journal-title":"Transactions of the American Mathematical Society"},{"key":"10.1016\/S1571-0661(04)00106-9_NEWBIB25","series-title":"Cambridge Summer School in Mathematical Logic","first-page":"253","article-title":"Combinator realizability of constructive finite type analysis","author":"Staples","year":"1973"},{"key":"10.1016\/S1571-0661(04)00106-9_NEWBIB26","series-title":"Habilitationsschrift","article-title":"Investigtations into intensional type theory","author":"Streicher","year":"1994"},{"key":"10.1016\/S1571-0661(04)00106-9_NEWBIB27","doi-asserted-by":"crossref","unstructured":"A.S. Troelstra. Notions of relizability for intuitionistic arithmetic and intuitionistic arithmetic in all finite types. In J.E. Fenstad, editor, The Second Scandinavian Logic Symposium, pages 369\u2013405. Northe-Holland, 1971.","DOI":"10.1016\/S0049-237X(08)70854-1"},{"key":"10.1016\/S1571-0661(04)00106-9_NEWBIB28","doi-asserted-by":"crossref","unstructured":"A.S. Troelstra editor. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Springer, 1973. With contributions by A.S. Troelstra, C.A. Smory\u0144ski, J.I. Zucker and W.A. Howard.","DOI":"10.1007\/BFb0066739"},{"key":"10.1016\/S1571-0661(04)00106-9_NEWBIB29","unstructured":"J. van Oosten. Excrcises in Realizability. PhD thesis, Universiteit van Amsterdam, 1991."},{"key":"10.1016\/S1571-0661(04)00106-9_NEWBIB30","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/BF01387763","article-title":"A semantical kproof of De DJongh's theorem","author":"van Oosten","year":"1991","journal-title":"Archive for Mathematical Logic"},{"key":"10.1016\/S1571-0661(04)00106-9_NEWBIB31","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1016\/S0168-0072(96)00050-4","article-title":"Extensional realizabilithy","volume":"84","author":"van Oosten","year":"1997","journal-title":"Annals of Pure and Applied Logic"},{"key":"10.1016\/S1571-0661(04)00106-9_NEWBIB32","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1016\/S0022-4049(97)00101-1","article-title":"The modified realizability topos","volume":"116","author":"van Oosten","year":"1997","journal-title":"Journal of pure and Applied Algebra"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104001069?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104001069?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:20Z","timestamp":1585571480000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104001069"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"references-count":32,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1999]]}},"alternative-id":["S1571066104001069"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)00106-9","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[1999]]}}}