{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:28:27Z","timestamp":1725488907990},"publisher-location":"London","reference-count":19,"publisher":"Springer London","isbn-type":[{"type":"print","value":"9783540197423"},{"type":"electronic","value":"9781447134947"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/978-1-4471-3494-7_2","type":"book-chapter","created":{"date-parts":[[2013,2,28]],"date-time":"2013-02-28T23:16:55Z","timestamp":1362093415000},"page":"13-26","source":"Crossref","is-referenced-by-count":2,"title":["Program Specification and Synthesis in Constructive Formal Systems"],"prefix":"10.1007","author":[{"given":"Pierangelo","family":"Miglioli","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ugo","family":"Moscato","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mario","family":"Ornaghi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"2_CR1","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1145\/2363.2528","volume":"1","author":"J Bates","year":"1985","unstructured":"Bates J., Constable R., Proofs as programs, ACM Transaction on Programming Languages and Systems (1), 1985, 113\u2013136.","journal-title":"ACM Transaction on Programming Languages and Systems"},{"key":"2_CR2","doi-asserted-by":"crossref","first-page":"127","DOI":"10.3233\/FI-1983-6202","volume":"IV.2","author":"A Bertoni","year":"1983","unstructured":"Bertoni A., Mauri G., Miglioli P., On the power of model theory to specify abstract data types and to capture their recursiveness, Fundamenta Informaticae IV.2, 1983, 127\u2013170.","journal-title":"Fundamenta Informaticae"},{"key":"2_CR3","first-page":"177","volume-title":"Semantics of data types (Sophia-Antipolis, 1984), Lecture Notes in Computer Science","author":"A Bertoni","year":"1984","unstructured":"Bertoni A., Mauri G., Miglioli P., Ornaghi M., Abstract data types and their extension within a constructive logic, in Kahn G., MacQueen D.B., Plotkin G. (eds), Semantics of data types (Sophia-Antipolis, 1984), Lecture Notes in Computer Science 173, Springer-Verlag,Berlin, 1984, 177\u2013195"},{"issue":"3","key":"2_CR4","first-page":"852","volume":"51","author":"P Bresciani","year":"1986","unstructured":"Bresciani P., Miglioli P., Moscato U., Ornaghi M., PAP: Proofs as Programs-(abstract), Journal of Symbolic Logic 51(3), 1986, 852\u2013853.","journal-title":"Journal of Symbolic Logic"},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"Bundy A., Smaill A., Wiggins G., The synthesis of logic programs from inductive proofs, in Lloyd J. (ed), Computational logic Springer-Verlag, 1990, 135-149.","DOI":"10.1007\/978-3-642-76274-1_8"},{"key":"2_CR6","unstructured":"Constable R., Allen S., Bromley H. et al., Implementing Mathematics with the Nuprl Development System, Prentice-Hall, 1986."},{"key":"2_CR7","unstructured":"Goad C., Computational uses of the manipulation of formal proofs, Rep. STAN-CS-80-819, Stanford University, 1980."},{"key":"2_CR8","unstructured":"Goguen J.A., Thatcher J.W., Wagner E.G., An initial algebra approach to the specification, correctness and implementation of abstract data types, IBM Res. Rep. RC6487, Yorktown Heights, 1976."},{"key":"2_CR9","unstructured":"Goto S., Program synthesis from natural deduction proofs, International Joint Conference on Artificial Intelligence, Tokyo, 1979, 339-341."},{"key":"2_CR10","volume-title":"Mathematics of program construction, Lecture Notes in Computer Science","author":"M Henson","year":"1989","unstructured":"Henson M., Realizability models for program construction, in J. van de Snepscheut, Mathematics of program construction, Lecture Notes in Computer Science 375, Springer-Verlag,Berlin, 1989"},{"key":"2_CR11","volume-title":"PX: A computational logic","author":"S Hiyashi","year":"1988","unstructured":"Hiyashi S., Nakano H., PX: A computational logic, MIT Press, Cambridge, 1988."},{"key":"2_CR12","volume-title":"Introduction to metamathematics","author":"S Kleene","year":"1952","unstructured":"Kleene S., Introduction to metamathematics, North Holland, Amsterdam, 1952."},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Lloyd J., Foundations of logic programming, Springer-Verlag, 1987.","DOI":"10.1007\/978-3-642-83189-8"},{"key":"2_CR14","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/S0049-237X(09)70189-2","volume-title":"VI International Congress for Logic, Methodology and Philosophy of Science","author":"P Martin-L\u00f6of","year":"1982","unstructured":"Martin-L\u00f6of P., Constructive Mathematics and Computer Programming, in L. Cohen, J. Los, H. Pfeiffer, K. Podewski (eds), VI International Congress for Logic, Methodology and Philosophy of Science, North-Holland, Amsterdam, 1982, 153\u2013179."},{"key":"2_CR15","unstructured":"Medvedev T., Finite problems, Sov. Math. Dok 3, 1962."},{"key":"2_CR16","first-page":"293","volume-title":"Mathematical Logic and its Applications","author":"P Miglioli","year":"1988","unstructured":"Miglioli P., Moscato U., Ornaghi M., Constructive theories with abstract data types for program synthesis, in Skordev D.G. (ed), Mathematical Logic and its Applications, Plenum Press, New York, 1988, 293\u2013302."},{"key":"2_CR17","first-page":"337","volume-title":"TAPSOFT\u2019 89, Lecture Notes in Computer Science","author":"P Miglioli","year":"1989","unstructured":"Miglioli P., Moscato U., Ornaghi M., Semi-constructive formal systems and axiomatization of abstract data types, in Diaz J., Orejas F. (eds), TAPSOFT\u2019 89, Lecture Notes in Computer Science 351, Springer-Verlag, Berlin, 1989, 337\u2013351."},{"key":"2_CR18","first-page":"1","volume":"IV","author":"P Miglioli","year":"1981","unstructured":"Miglioli P., Ornaghi M., A logically justified model of computation I,II, Fundamenta Informaticae IV. 1, 2, 1981.","journal-title":"Fundamenta Informaticae"},{"key":"2_CR19","unstructured":"Sato M., Towards a mathematical theory of program synthesis, International Joint Conference on Artificial Intelligence, Tokyo, 1979, 757-762."}],"container-title":["Workshops in Computing","Logic Program Synthesis and Transformation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-1-4471-3494-7_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,2,9]],"date-time":"2022-02-09T13:46:33Z","timestamp":1644414393000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-1-4471-3494-7_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540197423","9781447134947"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-1-4471-3494-7_2","relation":{},"ISSN":["1431-1682"],"issn-type":[{"type":"print","value":"1431-1682"}],"subject":[],"published":{"date-parts":[[1992]]}}}