{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:56:52Z","timestamp":1725663412156},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540509394"},{"type":"electronic","value":"9783540461166"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1989]]},"DOI":"10.1007\/3-540-50939-9_142","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T15:34:55Z","timestamp":1330184095000},"page":"337-351","source":"Crossref","is-referenced-by-count":0,"title":["Semi-constructive formal systems and axiomatization of abstract data types"],"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","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"22_CR1","doi-asserted-by":"crossref","unstructured":"Bates J., Constable R. \u2014 Proofs as programs \u2014 ACM Transaction on Programming Languages and Systems, vol. 7, n.1, 1985.","DOI":"10.1145\/2363.2528"},{"key":"22_CR2","unstructured":"Bertoni A., Mauri G., Miglioli P., Wirsing M. \u2014 On different approaches to abstract data types and the existence of recursive models \u2014 EATCS bulletin vol. 9, oct. 1979."},{"issue":"2","key":"22_CR3","doi-asserted-by":"crossref","first-page":"127","DOI":"10.3233\/FI-1983-6202","volume":"IV","author":"A. Bertoni","year":"1983","unstructured":"Bertoni A., Mauri G., Miglioli P. \u2014 On the power of model theory to specify abstract data types and to capture their recursiveness \u2014 Fundamenta Informaticae IV.2, 1983, pp. 127\u2013170.","journal-title":"Fundamenta Informaticae"},{"key":"22_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1007\/3-540-13346-1_9","volume-title":"Abstract data types and their extension within a constructive logic \u2014 Semantics of data types (Valbonne, 1984)","author":"A. Bertoni","year":"1984","unstructured":"Bertoni A., Mauri G., Miglioli P., Ornaghi M. \u2014 Abstract data types and their extension within a constructive logic \u2014 Semantics of data types (Valbonne, 1984), Lecture Notes in Computer Science, vol. 173, Springer-Verlag, Berlin, 1984, pp. 177\u2013195."},{"issue":"3","key":"22_CR5","first-page":"852","volume":"51","author":"P. Bresciani","year":"1986","unstructured":"Bresciani P., Miglioli P., Moscato U., Ornaghi M. \u2014 PAP: Proofs as Programs \u2014 (abstract), JSL, Vol. 51, n.3, 1986, pp. 852\u2013853.","journal-title":"JSL"},{"key":"22_CR6","series-title":"Lecture Notes in Comp. Sci.","volume-title":"Formalization of programming concepts","author":"M. Broy","year":"1981","unstructured":"Broy M., Wirsing M. \u2014 On the algebraic extension of abstract data types \u2014 in: Diaz J., Ramos I. (ed.) \u2014 Formalization of programming concepts \u2014 Lecture Notes in Comp. Sci. vol. 107, Springer-Verlag, Berlin, 1981."},{"key":"22_CR7","unstructured":"Chang C.C., Keisler H.J. \u2014 Model theory \u2014 North-Holland, 1973."},{"key":"22_CR8","unstructured":"Girard J. \u2014 The system F of variable types 15 years later \u2014 Report of CNRS, Paris, 1985."},{"key":"22_CR9","unstructured":"Goad C. \u2014 Computational uses of the manipulation of formal proofs \u2014 Rep. STAN-CS-80-819, Stanford University, 1980."},{"key":"22_CR10","unstructured":"Goguen J.A., Thatcher J.W., Wagner E.G. \u2014 An initial algebra approach to the specification, correctness and implementation of abstract data types \u2014 IBM Res. Rep. RC6487, Yorktown Heights, 1976."},{"key":"22_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"302","DOI":"10.1007\/3-540-09541-1_32","volume-title":"Program synthesis through G\u00f6del's interpretation \u2014 Mathematical studies of information processing","author":"S. Goto","year":"1979","unstructured":"Goto S. \u2014 Program synthesis through G\u00f6del's interpretation \u2014 Mathematical studies of information processing, (proceedings, Kyoto, 1978), Lecture Notes in Computer Science, vol.75, Springer-Verlag, Berlin, 1979, pp. 302\u2013325."},{"key":"22_CR12","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1007\/BF00260922","volume":"10","author":"J. Guttag","year":"1978","unstructured":"Guttag J., Horning J. \u2014 The algebraic specification of abstract data types \u2014 Acta Informatica 10, 27\u201352, 1978.","journal-title":"Acta Informatica"},{"key":"22_CR13","volume-title":"essays on combinatory logic, lambda calculus and formalism","author":"W.A. Howard","year":"1980","unstructured":"Howard W.A. \u2014 The formulae-as-types notion of construction \u2014 in To Curry H.B.: essays on combinatory logic, lambda calculus and formalism, Academic Press, London, 1980."},{"issue":"1","key":"22_CR14","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1305\/ndjfl\/1093883567","volume":"23","author":"R.E. Kirk","year":"1982","unstructured":"Kirk R.E. \u2014 A result on propositional logics having the disjunction property \u2014 Notre Dame Journal of Formal Logic, 23,1, 71\u201374, 1982.","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"22_CR15","doi-asserted-by":"crossref","first-page":"74","DOI":"10.1007\/BF01988049","volume":"3","author":"G. Kreisel","year":"1957","unstructured":"Kreisel G., Putnam H. \u2014 Eine unableitbarkeitsbeismethode f\u00fcr den intuitionistischen Aussagenkalkul \u2014 Archiv f\u00fcr Mathematische Logik und Grundlagenforschung, 3, 74\u201378, 1957.","journal-title":"Archiv f\u00fcr Mathematische Logik und Grundlagenforschung"},{"key":"22_CR16","first-page":"153","volume-title":"Logic, Methodology and Philosophy of Science VI","author":"P. Martin-L\u00f6f","year":"1982","unstructured":"Martin-L\u00f6f P. \u2014 Constructive Mathematics and Computer Programming \u2014 Logic, Methodology and Philosophy of Science VI, L. Cohen, J. Los, H. Pfeiffer, K. Podewski (ed.), North-Holland, Amsterdam, 1982, pp.153\u2013175."},{"key":"22_CR17","first-page":"293","volume-title":"Proceedings of the symposium Mathematical Logic and its Applications","author":"P. Miglioli","year":"1988","unstructured":"Miglioli P., Moscato U., Ornaghi M. \u2014 Constructive theories with abstract data types for program synthesis \u2014 Proceedings of the symposium Mathematical Logic and its Applications, Plenum Press, New York, 1988, pp.293\u2013302."},{"issue":"1","key":"22_CR18","first-page":"2","volume":"IV","author":"P. Miglioli","year":"1981","unstructured":"Miglioli P., Ornaghi M. \u2014 A logically justified model of computation I,II \u2014 Fundamenta Informaticae, IV.1,2, 1981.","journal-title":"Fundamenta Informaticae"},{"issue":"3","key":"22_CR19","doi-asserted-by":"crossref","first-page":"288","DOI":"10.1007\/BF02136027","volume":"24","author":"B. Nordstrom","year":"1984","unstructured":"Nordstrom B., Smith J.M. \u2014 Propositions, Types and Specifications of Programs in Martin-L\u00f6f's Type Theory \u2014 BIT, Vol. 24, n.3 1984, pp.288\u2013301.","journal-title":"BIT"},{"key":"22_CR20","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0066739","volume-title":"Metamathematical investigation of Intuitionistic Arithmetic and Analysis","author":"A.S. Troelstra","year":"1973","unstructured":"Troelstra A.S. \u2014 Metamathematical investigation of Intuitionistic Arithmetic and Analysis \u2014 Lecture Notes in Mathematics, vol.344, Springer-Verlag, Berlin, 1973."},{"key":"22_CR21","volume-title":"Handbook of Mathematical Logic","author":"A.S. Troelstra","year":"1977","unstructured":"Troelstra A.S. \u2014 Aspects of constructive mathematics \u2014 in: Barwise J. (ed.) \u2014 Handbook of Mathematical Logic, North Holland, Amsterdam 1977."},{"key":"22_CR22","doi-asserted-by":"crossref","unstructured":"Miglioli P., Moscato U., Ornaghi M. \u2014 PAP: a logic programming system based on a constructive logic \u2014 LNCS, n.306, Springer Verlag, 1988, pp.143\u2013156.","DOI":"10.1007\/3-540-19129-1_6"}],"container-title":["Lecture Notes in Computer Science","TAPSOFT '89"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-50939-9_142.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,30]],"date-time":"2021-12-30T21:42:09Z","timestamp":1640900529000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-50939-9_142"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1989]]},"ISBN":["9783540509394","9783540461166"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-50939-9_142","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1989]]}}}