{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:14:17Z","timestamp":1725455657399},"publisher-location":"Berlin\/Heidelberg","reference-count":14,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540571841"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0022578","type":"book-chapter","created":{"date-parts":[[2005,11,13]],"date-time":"2005-11-13T01:14:45Z","timestamp":1131844485000},"page":"301-312","source":"Crossref","is-referenced-by-count":1,"title":["A construction of typed lambda models related to feasible computability"],"prefix":"10.1007","author":[{"given":"Vladimir","family":"Sazonov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"32_CR1","doi-asserted-by":"crossref","unstructured":"S.R. Buss. The polynomial hierarchy and intuitionistic bounded arithmetic. In Structure in Complexity Theory, volume 223 of Lecture Notes in Computer Science, pages 77\u2013103, 1986.","DOI":"10.1007\/3-540-16486-3_91"},{"key":"32_CR2","first-page":"23","volume-title":"volume 298 of Lecture Notes in Computer Science","author":"A. Carboni","year":"1988","unstructured":"A. Carboni, P. Freyd, and A. Scedrov. A categorical approach to realizability and polymorphic types. In M. Main e.a., editors, Proceedings of 3rd ACM Workshop on Mathematical Foundations of Programming Languages Semantics, volume 298 of Lecture Notes in Computer Science, pages 23\u201342. Springer Verlag, New Orleans, 1988."},{"key":"32_CR3","doi-asserted-by":"crossref","unstructured":"S. Cook and A. Urquhart. Functional interpretations of feasibly constructive arithmetic. In Proc. 21st ACM STOC, pages 107\u2013112, 1989.","DOI":"10.1145\/73007.73017"},{"key":"32_CR4","volume-title":"Introduction to Metamathematics","author":"S.C. Kleene","year":"1952","unstructured":"S.C. Kleene. Introduction to Metamathematics. Van Nostrand P.C., Amsterdam, 1952."},{"issue":"4","key":"32_CR5","doi-asserted-by":"crossref","first-page":"1319","DOI":"10.2307\/2274281","volume":"49","author":"G. Longo","year":"1984","unstructured":"G.Longo and E.Moggi. The hereditary partial effective functionals and recursion theory in higher types. The Journal of Symbolic Logic, 49(4) 1319\u20131332, 1984.","journal-title":"The Journal of Symbolic Logic"},{"issue":"3","key":"32_CR6","first-page":"851","volume":"51","author":"J.C. Mitchell","year":"1986","unstructured":"J.C. Mitchell. Abstract realizability for intuitionistic and relevant implication (abstract). Journal of Symbolic Logic, 51(3):851\u2013852, 1986.","journal-title":"Journal of Symbolic Logic"},{"key":"32_CR7","doi-asserted-by":"crossref","unstructured":"J.C. Mitchell. Type systems for programming languages. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 8, pages 367\u2013458. Elsevier Science, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50013-5"},{"key":"32_CR8","volume-title":"Theoretical Aspects of Reasoning about Knowledge","author":"J.C. Mitchell","year":"1986","unstructured":"J.C. Mitchell and M.J. O'Donnel. Realizability semantics for errortolerant logics. In Theoretical Aspects of Reasoning about Knowledge. Morgan Kaufman, Los Altos, CA, 1986."},{"key":"32_CR9","volume-title":"Theory of recursive functions and effective computability","author":"H. Rogers Jr.","year":"1967","unstructured":"H.Jr.Rogers. Theory of recursive functions and effective computability. McGraw-Hill, New York, 1967"},{"key":"32_CR10","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1007\/978-1-4613-0609-2_25","volume-title":"Mathematical Logic","author":"V. Sazonov","year":"1990","unstructured":"V.Yu. Sazonov. An equivalence between polynomial constructivity of Markov's principle and the equality P = NP. In P. Petkov, editor, Mathematical Logic, Proceedings of the Summer School and Conference on Mathematical Logic, Dedicated to the Ninetieth Anniversary of Arend Heyting, held in 1988, Varna, Bulgaria, pages 351\u2013360. Plenum Press, NY, 1990. (A short English version.)"},{"key":"32_CR11","unstructured":"V.Yu. Sazonov and D.I. Sviridenko. Denotational semantics of the language of \u2211-expressions (in Russian). In Logical Problems in the Theory of Data Types, volume 114 of Vychislitelnye sistemy, pages 16\u201334. Novosibirsk, 1986."},{"key":"32_CR12","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/S0019-9958(85)80001-2","volume":"65","author":"R. Statman","year":"1985","unstructured":"R. Statman. Logical relations and the typed \u03bb-calculus. Information and Control, volume 65, pages 85\u201397, 1985.","journal-title":"Information and Control"},{"key":"32_CR13","doi-asserted-by":"crossref","unstructured":"A.A. Voronkov. Towards the theory of programming in constructive logic. In N. Jones, editor, Proc. of the European Symp. on Programming, volume 432 of Lecture Notes in Computer Science, pages 421\u2013435. Springer Verlag, 1990.","DOI":"10.1007\/3-540-52592-0_78"},{"key":"32_CR14","unstructured":"A.A. Voronkov. N-realizability: one more constructive semantics. Technical Report 71, Department of Mathematics, Monash University, 1991."}],"container-title":["Lecture Notes in Computer Science","Computational Logic and Proof Theory"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0022578.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T16:49:09Z","timestamp":1607532549000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0022578"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540571841"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/bfb0022578","relation":{},"subject":[]}}