{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T14:14:51Z","timestamp":1725459291540},"publisher-location":"Berlin\/Heidelberg","reference-count":29,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540555536"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0035165","type":"book-chapter","created":{"date-parts":[[2006,1,25]],"date-time":"2006-01-25T10:20:01Z","timestamp":1138184401000},"page":"43-54","source":"Crossref","is-referenced-by-count":0,"title":["Higher order functions in first order logics"],"prefix":"10.1007","author":[{"given":"Andrei","family":"Voronkov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"D.A. Basin. Building theories in Nuprl. In Logic at Botic'89, volume 363 of Lecture Notes in Computer Science, pages 12\u201325, 1989.","DOI":"10.1007\/3-540-51237-3_3"},{"key":"5_CR2","unstructured":"C.C.Chang and H.J.Keisler. Model theory. North Holland, 1977."},{"issue":"1","key":"5_CR3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0167-6423(87)90002-5","volume":"8","author":"P. Chisholm","year":"1987","unstructured":"P. Chisholm. Derivation of a parsing algorithm in Martin-L\u00f6f's theory of types. Science of Computer Programming, 8(1):1\u201342, 1987.","journal-title":"Science of Computer Programming"},{"key":"5_CR4","unstructured":"R.L. Constable and e.a. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, 1986."},{"issue":"213","key":"5_CR5","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"74","author":"T. Coquand","year":"1988","unstructured":"T. Coquand and G. Huet. The calculus of constructions. Information and computation, 74(213):95\u2013120, 1988.","journal-title":"Information and computation"},{"key":"5_CR6","volume-title":"The Theory of Enumerations (in Russian)","author":"Y. Ershov","year":"1977","unstructured":"Yu.L. Ershov. The Theory of Enumerations (in Russian). Nauka, Moscow, 1977."},{"key":"5_CR7","volume-title":"Decidability Problems and Constructive Models (in Russian)","author":"Y. Ershov","year":"1980","unstructured":"Yu.L. Ershov. Decidability Problems and Constructive Models (in Russian). Nauka, Moscow, 1980."},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"C.A. Goad. Proofs as descriptions of computation. In 5th CADE, volume 87 of Lecture Notes in Computer Science, pages 39\u201352, 1980.","DOI":"10.1007\/3-540-10009-1_4"},{"key":"5_CR9","unstructured":"C.A. Goad. Computational uses of the manipulation of formal proofs. Technical Report TR no. STAN-CS-80-819, Stanford Univ. Department of Computer Science, 1980."},{"key":"5_CR10","doi-asserted-by":"crossref","first-page":"27","DOI":"10.2307\/2964334","volume":"17","author":"R. Harrop","year":"1960","unstructured":"R. Harrop. Concerning formulas of the types A\u2192B\u2227C, A\u2192(Ex)B(x) in intuitionistic formal system. J. of Symb. Logic, 17:27\u201332, 1960.","journal-title":"J. of Symb. Logic"},{"key":"5_CR11","unstructured":"S. Hayashi and H. Nakano. PX: a Computational Logic. MIT Press, 1988."},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"M.C. Henson. Safe positive induction in the programming logic TK. In A.Voronkov, editor, 1st and 2nd Russian Conferences on Logic Programming, Lecture Notes in Artificial Intelligence, pages 215\u2013231. Springer Verlag, 1992.","DOI":"10.1007\/3-540-55460-2_16"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"J.Barwise. Admissible Sets and Structures. Springer Verlag, 1975.","DOI":"10.1007\/978-3-662-11035-5"},{"key":"5_CR14","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":"3","key":"5_CR15","first-page":"149","volume":"26","author":"J.-L. Krivine","year":"1990","unstructured":"J.-L. Krivine and M. Parigot. Programming with proofs. J.Inf.Proces. Cybern. EIK, 26(3):149\u2013167, 1990.","journal-title":"J.Inf.Proces. Cybern. EIK"},{"key":"5_CR16","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1090\/S0002-9947-1947-0025420-1","volume":"61","author":"D. Nelson","year":"1947","unstructured":"D. Nelson. Recursive functions and intuitionistic number theory. Trans. Amer. Math. Soc., 61:307\u2013368, 1947.","journal-title":"Trans. Amer. Math. Soc."},{"key":"5_CR17","first-page":"159","volume-title":"Trudy Instituta Matematiki","author":"N.N. Nepeivoda","year":"1982","unstructured":"N.N. Nepeivoda and D.I. Sviridenko. Towards the Theory for Program Synthesis (in Russian), volume 2 of Trudy Instituta Matematiki, pages 159\u2013175. Nauka, Novosibirsk, 1982."},{"issue":"3","key":"5_CR18","doi-asserted-by":"crossref","first-page":"288","DOI":"10.1007\/BF02136027","volume":"24","author":"B. Nordstr\u00f6m","year":"1984","unstructured":"B. Nordstr\u00f6m and J.M. Smith. Propositions, types and specifications of programs in Martin-L\u00f6f's type theory. BIT, 24(3):288\u2013301, 1984.","journal-title":"BIT"},{"issue":"3","key":"5_CR19","first-page":"636","volume":"42","author":"V.E. Plisko","year":"1978","unstructured":"V.E. Plisko. Some variants of realizability for predicate formulas. Izvestiya Akademii Nauk SSSR, Mathematics, 42(3):636\u2013653, 1978.","journal-title":"Izvestiya Akademii Nauk SSSR, Mathematics"},{"key":"5_CR20","first-page":"154","volume-title":"Soviet Conference on Applications of Mathematical Logic","author":"V.E. Plisko","year":"1986","unstructured":"V.E. Plisko. Towards a model theory for languages with constructive semantics (in Russian). In Soviet Conference on Applications of Mathematical Logic, pages 154\u2013156, Tallinn, 1986. Institute of Cybernetics."},{"key":"5_CR21","volume-title":"Natural deduction","author":"D. Prawitz","year":"1965","unstructured":"D. Prawitz. Natural deduction. Almquist and Wicksell, Stockholm, 1965."},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"D.S. Scott. Domains for denotational semantics. In Automata, Languages and Programming, volume 140 of Lecture Notes in Computer Science, pages 577\u2013612, 1982.","DOI":"10.1007\/BFb0012801"},{"key":"5_CR23","unstructured":"Soft Warehouse Inc. MULISP Reference Manual, 1989."},{"key":"5_CR24","unstructured":"S. Sokolowski. Applicative high-order programming or standard ML in the battlefield. Technical report, Universit\u00e4t Passau, Fakult\u00e4t f\u00fcr Mathematik und Informatik, 1989."},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"S.S. Starchenko and A. Voronkov. On connections between classical and constructive semantics. In COLOG-88, volume 417 of Lecture Notes in Computer Science, 1990.","DOI":"10.1007\/3-540-52335-9_59"},{"key":"5_CR26","first-page":"25","volume-title":"Trudy Instituta Matematiki","author":"A.A. Voronkov","year":"1988","unstructured":"A.A. Voronkov. Model theory based on a constructive notion of truth, (in Russian), volume 8 of Trudy Instituta Matematiki, pages 25\u201342. Nauka, Novosibirsk, 1988. This volume was cover-to-cover translated to English by American Mathematical Society."},{"key":"5_CR27","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":"5_CR28","unstructured":"A.A. Voronkov. N-realizability: one more constructive semantics. Technical Report 71, Department of Mathematics, Monash University, 1991."},{"key":"5_CR29","unstructured":"A.A. Voronkov. On completeness of program synthesis systems. Technical Report 29, Univ. Paris 7, Equipe de Logique Mathematique, 1991."}],"container-title":["Lecture Notes in Computer Science","Theory of Computing and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0035165.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T17:13:13Z","timestamp":1607533993000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0035165"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540555536"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/bfb0035165","relation":{},"subject":[]}}