{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T10:13:03Z","timestamp":1773655983881,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540657651","type":"print"},{"value":"9783540489580","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48958-4_5","type":"book-chapter","created":{"date-parts":[[2007,7,23]],"date-time":"2007-07-23T02:11:42Z","timestamp":1185156702000},"page":"81-100","source":"Crossref","is-referenced-by-count":4,"title":["Synthesis of Programs in Abstract Data Types"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Avellone","sequence":"first","affiliation":[]},{"given":"Mauro","family":"Ferrari","sequence":"additional","affiliation":[]},{"given":"Pierangelo","family":"Miglioli","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[1999,4,30]]},"reference":[{"key":"5_CR1","volume-title":"PhD thesis","author":"A. Avellone","year":"1998","unstructured":"A. Avellone. The algorithmic content of constructive proofs: translating proof s into programs and interpreting proofs as programs. PhD thesis, Dipartimento di Scienze dell\u2019Informazione, Universit\u00e0 degli Studi di Milano, Italy, 1998."},{"issue":"1","key":"5_CR2","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1145\/2363.2528","volume":"7","author":"J. Bates","year":"1985","unstructured":"J. Bates and R. Constable. Proof as programs. ACM Transaction on Programming Languages and Systems, 7(1):113\u2013136, 1985.","journal-title":"ACM Transaction on Programming Languages and Systems"},{"key":"5_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1007\/3-540-61780-9_60","volume-title":"The greatest common divisor: A case study for program extraction from classical proofs","author":"U. Berger","year":"1996","unstructured":"U. Berger and H. Schwichtenberg. The greatest common divisor: A case study for program extraction from classical proofs. Lecture Notes in Computer Science, 1158:36\u201346, 1996."},{"issue":"2","key":"5_CR4","doi-asserted-by":"crossref","first-page":"127","DOI":"10.3233\/FI-1983-6202","volume":"VI","author":"A. Bertoni","year":"1983","unstructured":"A. Bertoni, G. Mauri, and P. Miglioli. On the power of model theory to specify abstract data types and to capture their recursiveness. Fundamenta Informaticae, VI(2):127\u2013170, 1983.","journal-title":"Fundamenta Informaticae"},{"key":"5_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1007\/3-540-13346-1_9","volume-title":"Semantics of data types","author":"A. Bertoni","year":"1984","unstructured":"A. Bertoni, G. Mauri, P. Miglioli, and M. Ornaghi. Abstract data types and their extension within a constructive logic. In G. Kahn, D.B. MacQueen, and G. Plotkin, editors, Semantics of data types, LNCS 173, pages 177\u2013195. Springer Verlag, 1984."},{"key":"5_CR6","first-page":"47","volume":"9","author":"A. Bertoni","year":"1979","unstructured":"A. Bertoni, G. Mauri, P. Miglioli, and M. Wirsing. On different approaches to abstract data types and the existence of recursive models. EATCS bulletin, 9:47\u201357, 1979.","journal-title":"EATCS bulletin"},{"key":"5_CR7","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-69962-7","volume-title":"Fundamentals of Algebraic Specifications 1","author":"H. Ehrig","year":"1985","unstructured":"H. Ehrig and B. Mahr. Fundamentals of Algebraic Specifications 1. Berlin: Springer-Verlag, 1985."},{"key":"5_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/3-540-10009-1_4","volume-title":"CADE 5","author":"C.A. Goad","year":"1980","unstructured":"C.A. Goad. Proofs as description of computation. In CADE 5, pages 39\u201352. Springer-Verlag, LNCS, 1980."},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"K.-K. Lau and M. Ornaghi. On specification frameworks and deductive synthesis of logic programs. In Logic Program Synthesis and Transformation. Proceedings of LOPSTR\u201994, Pisa, Italy, 1994.","DOI":"10.1007\/3-540-58792-6_7"},{"key":"5_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"152","DOI":"10.1007\/3-540-60939-3_11","volume-title":"Towards an object-oriented methodology for deductive synthesis of logic programs","author":"K.-K. Lau","year":"1996","unstructured":"K.-K. Lau and M. Ornaghi. Towards an object-oriented methodology for deductive synthesis of logic programs. Lecture Notes in Computer Science, 1048:152\u2013169, 1996."},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"P. Miglioli, U. Moscato, and M. Ornaghi. Program specification and synthesis in constructive formal systems. In K.-K. Lau and T.P. Clement, editors, Logic Program Synthesis and Transformation, Manchester 1991, pages 13\u201326. Springer-Verlag, 1991. Workshops in Computing.","DOI":"10.1007\/978-1-4471-3494-7_2"},{"key":"5_CR12","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1006\/jsco.1994.1036","volume":"18","author":"P. Miglioli","year":"1994","unstructured":"P. Miglioli, U. Moscato, and M. Ornaghi. Abstract parametric classes and abstract data types defined by classical and constructive logical methods. Journal of Symbolic Computation, 18:41\u201381, 1994.","journal-title":"Journal of Symbolic Computation"},{"issue":"1","key":"5_CR13","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1305\/ndjfl\/1093634996","volume":"30","author":"P. Miglioli","year":"1989","unstructured":"P. Miglioli, U. Moscato, M. Ornaghi and G. Usberti. A constructivism based on classical truth. Notre Dame Journal of Formal Logic, 30(1): 67\u201390, 1989.","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"5_CR14","doi-asserted-by":"crossref","first-page":"151","DOI":"10.3233\/FI-1981-4108","volume":"IV","author":"P. Miglioli","year":"1981","unstructured":"P. Miglioli and M. Ornaghi. A logically justified model of computation. Fundamenta Informaticae, IV,1,2:151\u2013172,277\u2013341, 1981.","journal-title":"Fundamenta Informaticae"},{"key":"5_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1007\/BFb0021084","volume-title":"Classical proofs as programs: How, what, and why","author":"C.R. Murthy","year":"1992","unstructured":"C.R. Murthy. Classical proofs as programs: How, what, and why. Lecture Notes in Computer Science, 613:71\u201388, 1992."},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"H. Schwichtenberg. Proofs as programs. In P. Aczel, H. Simmons, and S. S. Wainer, editors, Proof Theory. A selection of papers from the Leeds Proof Theory Programme 1990, pages 81\u2013113. Cambridge University Press, 1993.","DOI":"10.1017\/CBO9780511896262.005"}],"container-title":["Lecture Notes in Computer Science","Logic-Based Program Synthesis and Transformation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48958-4_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,20]],"date-time":"2021-08-20T07:37:28Z","timestamp":1629445048000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48958-4_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540657651","9783540489580"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-48958-4_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[1999]]}}}