{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:03:30Z","timestamp":1725663810885},"publisher-location":"Berlin, Heidelberg","reference-count":61,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540525929"},{"type":"electronic","value":"9783540470458"}],"license":[{"start":{"date-parts":[[1990,1,1]],"date-time":"1990-01-01T00:00:00Z","timestamp":631152000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1990]]},"DOI":"10.1007\/3-540-52592-0_78","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T21:39:49Z","timestamp":1330205989000},"page":"421-435","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Towards the theory of programming in constructive logic"],"prefix":"10.1007","author":[{"given":"A. A.","family":"Voronkov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"26_CR1","first-page":"12","volume":"363","author":"D.A. Basin","year":"1989","unstructured":"Basin D.A. [1989]. Building theories in Nuprl. \u2014 In: Logic at Botic'89, LNCS 363, 1989, 12\u201325.","journal-title":"LNCS"},{"issue":"1","key":"26_CR2","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1145\/2363.2528","volume":"7","author":"J.L. Bates","year":"1985","unstructured":"Bates J.L., Constable R.L. [1985] Proofs as programs. \u2014 ACM Trans. on Programming languages and systems, 1985, v.7, no.1, p.113\u2013136.","journal-title":"ACM Trans. on Programming languages and systems"},{"issue":"2","key":"26_CR3","doi-asserted-by":"crossref","first-page":"228","DOI":"10.2307\/2272821","volume":"43","author":"M. J. Beeson","year":"1978","unstructured":"Beeson M. J. [1978a] Some relations between classical and constructive mathematics. \u2014 J. Symb. Logic, 1978, v.43, no.2, p.228\u2013246.","journal-title":"J. Symb. Logic"},{"key":"26_CR4","doi-asserted-by":"crossref","unstructured":"Beeson M.J. [1986] Proving programs and programming proofs. \u2014 In: VII Int. Congress on Logic, Methodology and Philosophy of Science, Elsevier Sci. Publishers, 1986, p.51\u201382.","DOI":"10.1016\/S0049-237X(09)70684-6"},{"key":"26_CR5","first-page":"177","volume":"173","author":"A. Bertoni","year":"1984","unstructured":"Bertoni A., Mauri G., Miglioli P., Ornaghi M. [1984] Abstract data types and their extension within a constructive logic. \u2014 Semantics of Data Types, LNCS 173, 1984, 177\u2013195.","journal-title":"LNCS"},{"key":"26_CR6","doi-asserted-by":"crossref","unstructured":"Bishop E. [1970] Mathematics as a numerical language. In: Intuitionism and Proof Theory, North Holland, 1970, p.53\u201371.","DOI":"10.1016\/S0049-237X(08)70740-7"},{"issue":"3","key":"26_CR7","first-page":"852","volume":"51","author":"P. Bresciani","year":"1986","unstructured":"Bresciani P., Miglioli P., Moscato U., Ornaghi M. [1986] PAP \u2014 proofs as programs (Abstract). \u2014 JSL 51(3), 1986, 852\u2013853.","journal-title":"JSL"},{"issue":"1","key":"26_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0167-6423(87)90002-5","volume":"8","author":"P. Chisholm","year":"1987","unstructured":"Chisholm P. [1987] Derivation of a parsing algorithm in Martin-Lof's theory of types. \u2014 Science of Computer Programming, 1987, v.8, no.1, p.1\u201342.","journal-title":"Science of Computer Programming"},{"key":"26_CR9","unstructured":"Constable R.L. [1972] Constructive mathematics and automatic program writers. \u2014 In: IFIP'71, North Holland, 1972, p.229\u2013233."},{"issue":"3","key":"26_CR10","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/0020-0190(83)90060-1","volume":"16","author":"R.L. Constable","year":"1983","unstructured":"Constable R.L. [1983] Programs as proofs: a synopsis. \u2014 Information Processing Letters, 1983, v.16, no.3, p.105\u2013112.","journal-title":"Information Processing Letters"},{"key":"26_CR11","unstructured":"Constable R.L. e.a. [1986] Implementing mathematics with the Nuprl proof development system. \u2014 Prentice Hall, 1986."},{"issue":"213","key":"26_CR12","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"74","author":"T. Coquand","year":"1988","unstructured":"Coquand T., Huet G. [1988] The calculus of constructions. \u2014 Information and computation, 1988, v.74, no.213, p.95\u2013120.","journal-title":"Information and computation"},{"key":"26_CR13","unstructured":"Dragalin A.G. [1967] To the basing of Markov's principle. \u2014 Soviet Mathematical Doklady, 1967, v.177."},{"key":"26_CR14","unstructured":"Dragalin A.G. [1978] Mathematical intuitionism. Introduction to the proof theory (Russian). \u2014 Moscow, Nauka, 1978."},{"key":"26_CR15","unstructured":"de Bruin N.G. [1980] A survey of the project AUTOMATH. \u2014 In: To H.B.Curry; Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, 1980, p.579\u2013606."},{"key":"26_CR16","first-page":"491","volume-title":"Festschrift on the occasion of H.B.Curry's 80th Birthday","author":"J. Diller","year":"1980","unstructured":"Diller J. [1980] Modified realization and the formulae-as-types notion. In: Festschrift on the occasion of H.B.Curry's 80th Birthday, Academic Press, N.Y., 1980, p.491\u2013502."},{"key":"26_CR17","doi-asserted-by":"crossref","unstructured":"Ershov Yu.L. [1973] The theory of A-spaces. \u2014 Algebra i Logica, 12(4), 1973.","DOI":"10.1007\/BF02218570"},{"key":"26_CR18","unstructured":"Ershov Yu.L. [1977] The theory of enumerations (in Russian). \u2014 Moscow, Nauka, 1977."},{"key":"26_CR19","unstructured":"Ershov Yu.L. [1980] Decidability problems and constructive models (in Russian). \u2014 Moscow, Nauka, 1980."},{"key":"26_CR20","doi-asserted-by":"crossref","unstructured":"Feferman S. [1979] Constructive theories of functions and classes. \u2014 In: Logic Colloquium'78, North Holland, 1979, p.159\u2013224.","DOI":"10.1016\/S0049-237X(08)71625-2"},{"key":"26_CR21","doi-asserted-by":"crossref","unstructured":"Feferman S. [1984] Between constructive and classical mathematics. \u2014 In: Computation and proof theory, Lecture Notes in Math 1104, 1984, p.143\u2013162.","DOI":"10.1007\/BFb0099484"},{"key":"26_CR22","first-page":"39","volume":"87","author":"C.A. Goad","year":"1980","unstructured":"Goad C.A. [1980a] Proofs as descriptions of computation. \u2014 5th CADE, LNCS 87, 1980, p.39\u201352.","journal-title":"5th CADE, LNCS"},{"key":"26_CR23","unstructured":"Goad C.A. [1980b] Computational uses of the manipulation of formal proofs. \u2014 Stanford Univ. Department of CS, TR no. STAN-CS-80-819, 1980, 122p."},{"issue":"3\/4","key":"26_CR24","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1111\/j.1746-8361.1958.tb01464.x","volume":"12","author":"K. G\u00f6del","year":"1958","unstructured":"G\u00f6del K. [1958] Uber eine noch nicht benutzte Erweiterung des finiten Standpunktes. \u2014 Dialectica, 1958, v.12, no. 3\/4, p.280\u2013287.","journal-title":"Dialectica"},{"key":"26_CR25","first-page":"339","volume":"1","author":"S. Goto","year":"1979","unstructured":"Goto S. [1979b] Program synthesis from natural deduction proofs. \u2014 6th IJCAI, 1979, v.1, p.339\u2013341.","journal-title":"6th IJCAI"},{"key":"26_CR26","doi-asserted-by":"crossref","first-page":"27","DOI":"10.2307\/2964334","volume":"17","author":"R. Harrop","year":"1960","unstructured":"Harrop R. [1960] Concerning formulas of the types A\u2192 BB V C, A \u2192 (Ex)B(x) in intuitionistic formal system. \u2014 J. Symb. Logic, v.17, 1960, pp.27\u201332.","journal-title":"J. Symb. Logic"},{"key":"26_CR27","unstructured":"Hayashi S., Nakano H. [1988] PX: a computational logic. \u2014 MIT Press, 1988."},{"key":"26_CR28","unstructured":"Henson M.C. [1989a] Information loss in the programming logic TK. \u2014 Draft, Univ. of Essex, Department of Computer Sci., October, 1989."},{"key":"26_CR29","first-page":"256","volume":"375","author":"M.C. Henson","year":"1989","unstructured":"Henson M.C. [1989b] Realizability models for program construction. \u2014 In: J.L.A. van de Snepsheut (Ed.), Mathematics of Program Construction, LNCS 375, 1989, 256\u2013272.","journal-title":"LNCS"},{"key":"26_CR30","unstructured":"Huet D. [1986] Computation and deduction. \u2014 Carnegie Mellon Univ., 1986."},{"key":"26_CR31","unstructured":"Kleene S.C. [1952] Introduction to metamathematics. \u2014 Van Nostrand P.C., Amsterdam, 1952."},{"key":"26_CR32","doi-asserted-by":"crossref","unstructured":"Kleene S.C. [1973] Realizability: a retrospective survey. \u2014 LNM 337, 1973.","DOI":"10.1007\/BFb0066772"},{"key":"26_CR33","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/BF01186549","volume":"35","author":"A.N. Kolmogorov","year":"1932","unstructured":"Kolmogorov A.N. [1932] Zur Deutung der Intuitionistischen Logik. \u2014 Mathematische Zeitschrift, v.35, 1932, p.58\u201365.","journal-title":"Mathematische Zeitschrift"},{"key":"26_CR34","unstructured":"Kreisel G. [1958] Interpretation of analysis by means of constructive functionals of finite types. \u2014 In: Constructivity in Mathematics, North Holland, 1958, p.101\u2013128."},{"key":"26_CR35","doi-asserted-by":"crossref","unstructured":"L\u00e4uchly H. [1970] An abstract notion of realizability for which intuitionistic predicate calculus is complete. \u2014 In: Intuitionism and Proof Theory, North Holland, 1970, p.227\u2013234.","DOI":"10.1016\/S0049-237X(08)70754-7"},{"issue":"4","key":"26_CR36","doi-asserted-by":"crossref","first-page":"294","DOI":"10.1109\/TSE.1979.234198","volume":"5","author":"Z. Manna","year":"1979","unstructured":"Manna Z., Waldinger R. [1979] Synthesis: dreams \u2192 programs. \u2014 IEEE Trans. Software Engineering, 1979, v.5, no.4, p. 294\u2013328.","journal-title":"IEEE Trans. Software Engineering"},{"key":"26_CR37","unstructured":"Markov A.A., Nagorny N.M. [1986] Theory of algorithms. \u2014 Moscow, Nauka, 1986."},{"key":"26_CR38","first-page":"337","volume":"351","author":"P. Miglioli","year":"1989","unstructured":"Miglioli P., Moscato U., Ornaghi M. [1989] Semi-constructive formal systems and axiomatization of abstract data types. \u2014 TAPSOFT'89, LNCS 351, 337\u2013351.","journal-title":"LNCS"},{"key":"26_CR39","first-page":"110","volume":"40","author":"G.E. Mints","year":"1974","unstructured":"Mints G.E. [1974] E-theorems (in Russian). \u2014 Zapiski Nauchnyh seminarov LOMI, 1974, v.40, p.110\u2013118.","journal-title":"Zapiski Nauchnyh seminarov LOMI"},{"key":"26_CR40","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1090\/S0002-9947-1947-0025420-1","volume":"61","author":"D. Nelson","year":"1947","unstructured":"Nelson D. [1947] Recursive functionals and intuitionistic number theory. \u2014 Trans. Amer. Math. Soc., v.61, 1947, p.307\u2013368.","journal-title":"Trans. Amer. Math. Soc."},{"key":"26_CR41","doi-asserted-by":"crossref","unstructured":"Nepeivoda N.N. [1979a] An application of proof theory to the problem of con structing correct programs. \u2014 Kibernetika, 1979, no.2.","DOI":"10.1007\/BF01069330"},{"key":"26_CR42","unstructured":"Nepeivoda N.N. [1979b] A method of constructing correct programs from correct subprograms. \u2014 Programmirovanie, 1979, no.1."},{"key":"26_CR43","unstructured":"Nepeivoda N.N., Sviridenko D.I. [1982] Towards the theory of program synthesis (in Russian). \u2014 In: Trudy Instituta Matematiki, v.2, Novosibirsk, Nauka, 1982, p.159\u2013175."},{"key":"26_CR44","unstructured":"Nordstrom B., Peterson K. [1983] Types and specifications. \u2014 IFIP'83, NH, 1983, 915\u2013920."},{"issue":"3","key":"26_CR45","doi-asserted-by":"crossref","first-page":"288","DOI":"10.1007\/BF02136027","volume":"24","author":"B. Nordstrom","year":"1984","unstructured":"Nordstrom B., Smith J.M. [1984] Propositions, types and specifications of programs in Martin-Lof's type theory. \u2014 BIT, 24(3), 1984, 288\u2013301.","journal-title":"BIT"},{"key":"26_CR46","unstructured":"Plisko V.E. [1987] On languages with constructive logical connectives. \u2014 Soviet Mathematical Doklady, v.296, no. 1., 1987."},{"key":"26_CR47","doi-asserted-by":"crossref","unstructured":"Prank R.K. [1981] Expressibility in elementary theory or recursively enumerable sets with realizability logic. \u2014 Algebra i Logica, 20(4), 1981.","DOI":"10.1007\/BF01669112"},{"key":"26_CR48","unstructured":"Prawitz D. Natural deduction. \u2014 Stockholm, Almquist and Wicksell, 1965."},{"key":"26_CR49","volume-title":"A programming system for type theory","author":"K. Petersson","year":"1982","unstructured":"Petersson K. [1982] A programming system for type theory. \u2014 LPM Memo 21, Dpt of CS, Chalmers Univ. of Technology, Goteborg, 1982."},{"key":"26_CR50","doi-asserted-by":"crossref","first-page":"577","DOI":"10.1007\/BFb0012801","volume":"140","author":"D.S. Scott","year":"1982","unstructured":"Scott D.S. [1982] Domains for denotational semantics. In: Lecture Notes in Computer Science 140, 1982, pp.577\u2013612.","journal-title":"Lecture Notes in Computer Science"},{"key":"26_CR51","unstructured":"Starchenko S.S., Voronkov A.A. [1988] On connections between classical and constructive semantics. \u2014 In: COLOG-88 (papers presented at the Int. Conf. on Computer Logic), Part 1, Tallinn, 1988, p.101\u2013112."},{"key":"26_CR52","unstructured":"Voronkov A.A. [1985] A generalization of the notion of realizability. \u2014 Unpublished Manuscript, 25pp. (Abstract was published in Siberian Mathematical Journal, 1986)."},{"key":"26_CR53","volume-title":"Logic programs and their synthesis","author":"A.A. Voronkov","year":"1986","unstructured":"Voronkov A.A. [1986a] Logic programs and their synthesis (Russian). Preprint no. 23, Institute of Mathematics, Novosibirsk, 1986."},{"key":"26_CR54","volume-title":"Synthesis of logic programs","author":"A.A. Voronkov","year":"1986","unstructured":"Voronkov A.A. [1986b] Synthesis of logic programs (Russian). Preprint no. 24, Institute of Mathematics, Novosibirsk, 1986."},{"key":"26_CR55","unstructured":"Voronkov A.A. [1986c] Intuitionistic list theory (Russian). \u2014 In: Abstracts of the 8th All-union Conf. on Mathematical Logic, Moscow, 1986."},{"key":"26_CR56","unstructured":"Voronkov A.A. [1987a] Constructive logic: a semantic approach. \u2014 In: Abstracts of the 8th Int. Congress on Logic, Methodology and Philosophy of Sci., v.5, part 1, Moscow, Nauka, 1987, p.79\u201382."},{"key":"26_CR57","first-page":"479","volume":"278","author":"A.A. Voronkov","year":"1987","unstructured":"Voronkov A.A. [1987b] Deductive program synthesis and Markov's principle. \u2014 In: Fundamentals of computation theory, LNCS v.278, 1987, p.479\u2013482.","journal-title":"LNCS"},{"key":"26_CR58","unstructured":"Voronkov A.A. [1988a] Constructive calculi and constructive models. \u2014 Soviet Mathematical Doklady, 299 (1), 1988."},{"key":"26_CR59","unstructured":"Voronkov A.A. [1988b] Model theory based on the constructive notion of truth. \u2014 In: Model Theory and Applications, Trudy Instituta Matematiki, v.8, Novosibirsk, 1988."},{"key":"26_CR60","unstructured":"Voronkov A.A. [1989a] Program synthesis using proofs in first order logic. (Russian). \u2014 To be published in Vychislitelnye sistemy, 1989, 50pp."},{"key":"26_CR61","unstructured":"Voronkov A.A. [1989b] A theory for programming in constructive logic. \u2014 presented to the 3rd Int. Conf. on Computer Sci. Logic, Kaiserslautern, October, 1989."}],"container-title":["Lecture Notes in Computer Science","ESOP '90"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-52592-0_78","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T18:02:44Z","timestamp":1687284164000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-52592-0_78"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990]]},"ISBN":["9783540525929","9783540470458"],"references-count":61,"URL":"https:\/\/doi.org\/10.1007\/3-540-52592-0_78","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1990]]},"assertion":[{"value":"1 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}