{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:58:28Z","timestamp":1725663508905},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540191292"},{"type":"electronic","value":"9783540391265"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1988]]},"DOI":"10.1007\/3-540-19129-1_6","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T20:04:09Z","timestamp":1330200249000},"page":"141-156","source":"Crossref","is-referenced-by-count":2,"title":["PAP: a logic programming system based on a constructive logic"],"prefix":"10.1007","author":[{"given":"P.","family":"Miglioli","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"U.","family":"Moscato","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.","family":"Ornaghi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"6_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":"6_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":"6_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":"6_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":"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":"6_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, no.3, 1986, pp. 852\u2013853.","journal-title":"(abstract), JSL"},{"key":"6_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":"6_CR7","unstructured":"Chang C.C., Keisler H.J. \u2014 Model theory \u2014 North-Holland, 1973."},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Constable R., Knoblock B., Bates J. \u2014 Writing programs that construct proofs \u2014 Journal of Automated Reasoning vol.1, n.3, 1985. D Reidel Pu. Co., 1981.","DOI":"10.1007\/BF00244273"},{"key":"6_CR9","unstructured":"Girard J. \u2014 Linear logic \u2014 report of CNRS, Paris, 1986."},{"key":"6_CR10","unstructured":"Goad C. \u2014 Computational uses of the manipulation of formal proofs \u2014 Rep. STAN-CS-80-819, Stanford University, 1980."},{"key":"6_CR11","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":"6_CR12","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, (proceedings, Kyoto, 1978)","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":"6_CR13","unstructured":"Kreisel G. \u2014 Some uses of proof-theory in finding computer programs \u2014 Notes for a talk in the Logical Symposium of Clermond Ferrand, 1976 (available as a manuscript)."},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Lloyd J. W. \u2014 Foundation of logic programming \u2014 Springer Verlag, 1984.","DOI":"10.1007\/978-3-642-96826-6"},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"Miglioli P., Moscato U., Ornaghi M. \u2014 Constructive theories with abstract data types for program synthesis \u2014 It will appear on the Proceedings of the symposium on Mathematical logic and its applications held in Druzhba (Bulgaria) on September 1986.","DOI":"10.1007\/978-1-4613-0897-3_21"},{"key":"6_CR16","first-page":"153","volume-title":"Constructive Mathematics and Computer Programming \u2014 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."},{"issue":"3","key":"6_CR17","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":"6_CR18","doi-asserted-by":"crossref","unstructured":"Thomason R. \u2014 A semantical study of constructible falsity \u2014 Zeitschrift fur matematische Logic und Grundlagen der Mathematik, Vol.15, 1969.","DOI":"10.1002\/malq.19690151602"},{"key":"6_CR19","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."}],"container-title":["Lecture Notes in Computer Science","Foundations of Logic and Functional Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-19129-1_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T02:27:11Z","timestamp":1640917631000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-19129-1_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1988]]},"ISBN":["9783540191292","9783540391265"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-19129-1_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1988]]}}}