{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:47:36Z","timestamp":1725662856475},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540108283"},{"type":"electronic","value":"9783540387169"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1981]]},"DOI":"10.1007\/3-540-10828-9_57","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T17:26:52Z","timestamp":1330190812000},"page":"101-116","source":"Crossref","is-referenced-by-count":5,"title":["Abstract data types and rewriting systems : Application to the programming of Algebraic Abstract Data Types in PROLOG"],"prefix":"10.1007","author":[{"given":"Marc","family":"Bergman","sequence":"first","affiliation":[]},{"given":"Pierre","family":"Deransart","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"7_CR1","unstructured":"A.L. FURTADO, P.A.S. VELOSO Procedural Verification and Implementations for Abstract Data Types, Pontificia Universidade Catolica do Rio de Janeiro. Private communication."},{"key":"7_CR2","unstructured":"M.C. GAUDEL Compiler Proof and Generation based on semantics of programming Languages (French) Th\u00e8se de Doctorat \u2014 10 th March 1980 \u2014 Nancy \u2014"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"J.A. GOGUEN. How to prove algebraic inductive hypotheses without induction with applications to the correctness of data type implementation. 5th Conference on Automated Deduction. Les Arcs, France, Juillet 1980. (LNCS 87, pp. 356\u2013373).","DOI":"10.1007\/3-540-10009-1_27"},{"key":"7_CR4","unstructured":"J.A. GOGUEN, J.J. TARDO, \"An introduction to OBJ, A Language for writing and testing Formal Algebraic Program Specification\". Specification of Reliable Software. Boston Apr. 1979. pp. 170\u2013189."},{"key":"7_CR5","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1007\/BF00260922","volume":"10","author":"J.V. Guttag","year":"1978","unstructured":"J.V. GUTTAG, J.J. HORNING, The Algebraic Specification of Abstract Data Types. Acta Informatica 10 (1978), 27\u201352.","journal-title":"Acta Informatica"},{"issue":"N6","key":"7_CR6","doi-asserted-by":"crossref","first-page":"396","DOI":"10.1145\/359605.359618","volume":"V20","author":"J. Guttag","year":"1977","unstructured":"J. GUTTAG Abstract Data Types and the Development of Data Structures. CACM \u2014 V20 \u2014 N6 \u2014 June 1977 \u2014 pp 396\u2013404.","journal-title":"CACM"},{"key":"7_CR7","unstructured":"G. HUET, J.M. HULLOT, Proofs by Induction in Equational Theories with Constructors. Rapport INRIA no28."},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"G. HUET, D. OPPEN Equations and Rewrite Rules: a Survey. \"Formal Languages: Perspectives and Open Problems\". Ed. Book R, Academic Press 1980. Also TR-CSL-111, SRI International, Jan. 1980.","DOI":"10.1016\/B978-0-12-115350-2.50017-8"},{"key":"7_CR9","unstructured":"E. MADELAINE, S. SENESI, On using LCF and PROLOG to prove Correctness of Abstract Data Type Representation (French). Ecole Polytechnique \u2014 INRIA \u2014 July 1980."},{"key":"7_CR10","unstructured":"D.R. MUSSER \"A Data Type Verification System Based on Rewrite Rules\". Proceedings of the Sixth Texas Conference"},{"key":"7_CR11","unstructured":"D.R. MUSSER, Convergent Set of Rewrite Rules for Abstract Data Types. USC \u2014 ISI. Californie. D\u00e9c. 78 \u2014 Nov. 79."},{"key":"7_CR12","unstructured":"C. PAIR On the Models of Algebraic Abstract Data Types (French) Centre de Recherche en Informatique de Nancy \u2014 Report 80 P 052, May 1980."},{"key":"7_CR13","unstructured":"P. ROUSSEL PROLOG Reference Manual (French) Universit\u00e9 d'Aix \u2014 Marseille II \u2014 Septembre 1975."}],"container-title":["Lecture Notes in Computer Science","CAAP '81"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-10828-9_57.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:03:28Z","timestamp":1605643408000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-10828-9_57"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1981]]},"ISBN":["9783540108283","9783540387169"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-10828-9_57","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1981]]}}}