{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:57:42Z","timestamp":1725663462727},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540164425"},{"type":"electronic","value":"9783540397823"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1986]]},"DOI":"10.1007\/3-540-16442-1_27","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T18:40:43Z","timestamp":1330195243000},"page":"351-374","source":"Crossref","is-referenced-by-count":2,"title":["Rewriting with a nondeterministic choice operator : From algebra to proofs"],"prefix":"10.1007","author":[{"given":"St\u00e9phane","family":"Kaplan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,29]]},"reference":[{"key":"27_CR1","unstructured":"J.A.Goguen, J.W. Thatcher, E.G.Wagner, An initial algebra approach to the specification, correctness and implementation of abstract data types, in Current Trends in Programming Methodology, Prentice-Hall N-J. (1978)"},{"key":"27_CR2","doi-asserted-by":"crossref","unstructured":"K.Apt, Ten years of Hoare's logic: a survey. Part II: nondeterminism, in Theoretical Computer Science 28 (1984).","DOI":"10.1016\/0304-3975(83)90066-X"},{"key":"27_CR3","unstructured":"J.Bergstra, J.Klop, Algebra of communicating processes with abstraction, CWI Report CS-R8403, Amsterdam (1984)."},{"key":"27_CR4","doi-asserted-by":"crossref","unstructured":"J.Bergstra, J.Klop, Algebra of communicating processes. Part II, CWI Report, Amsterdam (1984)","DOI":"10.1016\/0304-3975(85)90088-X"},{"key":"27_CR5","unstructured":"M. Bidoit, Une methode de presentation de types abstraits: applications, These de 3e cycle, Orsay (1981)"},{"key":"27_CR6","unstructured":"R. Boyer, J.S. Moore, A computational logic, Academic Press, (1979)."},{"key":"27_CR7","volume-title":"An \"asynchronous\" calculus MEIJE","author":"G. Boudol","year":"1984","unstructured":"G. Boudol, An \"asynchronous\" calculus MEIJE, in NATO Summer School, La-Colle-sur-Loup, France (1984)."},{"key":"27_CR8","doi-asserted-by":"crossref","unstructured":"L.Bachmai, D.Plaisted, Associative path orderings, Proc. 1st RTA Conf., Dijon (1985).","DOI":"10.1016\/S0747-7171(85)80019-5"},{"key":"27_CR9","unstructured":"S.D.Brookes, On the relationship between CCS and CSP, Proc. 10th ICALP Conf., L.N.C.S., Springer Verlag (1983)."},{"key":"27_CR10","doi-asserted-by":"crossref","unstructured":"M.Broy, On the Herbrand Kleene universe for nondeterministic computations, Proc. MFCS 84 Conf., L.N.C.S., Springer Verlag (1984).","DOI":"10.1007\/BFb0030301"},{"key":"27_CR11","doi-asserted-by":"crossref","unstructured":"M.Broy, M.Wirsing, On the algebraic specification of nondeterministic programming languages, Proc. CAAP-81 Conf., L.N.C.S. N.112 (1981).","DOI":"10.1007\/3-540-10828-9_61"},{"key":"27_CR12","doi-asserted-by":"crossref","unstructured":"C.Choppy, C.Johnen, Petrireve: proving Petri net properties with rewriting systems, Proc. 1st RTA Conf., Dijon (1985).","DOI":"10.1007\/3-540-15976-2_13"},{"key":"27_CR13","doi-asserted-by":"crossref","unstructured":"N. Dershowitz, Orderings for term rewriting systems, Proc. 20th Symposium on Foundation of Computer Science, pp.123\u2013131 (1979).","DOI":"10.1109\/SFCS.1979.32"},{"key":"27_CR14","doi-asserted-by":"crossref","unstructured":"D.Detlefs, R.Forgaard, A procedure for automatically proving the termination of a set of rewrite rules, Proc. 1st RTA Conf., Dijon (1985).","DOI":"10.1007\/3-540-15976-2_12"},{"key":"27_CR15","doi-asserted-by":"crossref","unstructured":"L.Fribourg, A narrowing procedure for theories with constructors, Proc. CADE Conf., Napa (1984).","DOI":"10.1007\/978-0-387-34768-4_16"},{"key":"27_CR16","doi-asserted-by":"crossref","unstructured":"J.Goguen, J.Meseguer, Completeness of many-sorted equational logic, SIGPLAN Notices (1981).","DOI":"10.1145\/947864.947865"},{"key":"27_CR17","doi-asserted-by":"crossref","unstructured":"J.Goguen, How to prove algebraic inductive hypotheses without induction, 5th CAD, Les Arcs-France (1980).","DOI":"10.1007\/3-540-10009-1_27"},{"key":"27_CR18","doi-asserted-by":"crossref","unstructured":"M.Hennessy, Powerdomains and nondeterministic recursive definitions, Symposium on Programming, L.N.C.S N.137 (1982)","DOI":"10.1007\/3-540-11494-7_13"},{"key":"27_CR19","unstructured":"G.Huet, Confluent reductions: abstract properties and applications to term rewriting systems, Proc. 18th FOCS Conf., Providence (1978)."},{"key":"27_CR20","doi-asserted-by":"crossref","unstructured":"G. Huet, J-M. Hullot, Proofs by induction in equational theories with constructors 21st FOCS (1980).","DOI":"10.1109\/SFCS.1980.37"},{"key":"27_CR21","unstructured":"G.Huet, D.C. Oppen, Equations and rewrite rules: a survey, Formal languages: Perspective and open problems, R. Book Ed., Academic Press (1980)."},{"key":"27_CR22","doi-asserted-by":"crossref","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"C. A. R. R. Hoare","year":"1978","unstructured":"C.A.R. Hoare, Communicating sequential processes, CACM 21 666\u2013677 (1978).","journal-title":"CACM"},{"key":"27_CR23","doi-asserted-by":"crossref","unstructured":"J.P.Jouannaud, C.Kirchner, Completion of a set of rules modulo a set of equations, Proc. of the 11th POPL Conference (1984).","DOI":"10.1145\/800017.800519"},{"key":"27_CR24","unstructured":"S. Kaplan, Unification, narrowing with fair conditional term rewriting systems, Internal L.R.I. Report (to appear)."},{"key":"27_CR25","unstructured":"S. Kaplan, A Birkhoff theorem for nondeterministic specifications, Weizmann Institute Internal Note, Rehovot (to appear-1986)"},{"key":"27_CR26","unstructured":"D.E. Knuth, P.B. Bendix, Simple word problems in universal algebra, Computational problems in abstract algebra, J.Leech Ed., Pergammon Press (1970)."},{"key":"27_CR27","doi-asserted-by":"crossref","unstructured":"C.Kirchner, A new equational unification method: a generalization of Martelli-Montanari's algorithm, Proc. CADE Conf. (1984).","DOI":"10.1007\/978-0-387-34768-4_14"},{"key":"27_CR28","doi-asserted-by":"crossref","unstructured":"P.Lescanne, Computer experiment with the REVE term rewriting systems generator, Proc. of the 10th POPL Conference (1983).","DOI":"10.1145\/567067.567078"},{"key":"27_CR29","doi-asserted-by":"crossref","unstructured":"R.Milner, A calculus of communicating systems, L.N.C.S. N.92, Springer Verlag (1980).","DOI":"10.1007\/3-540-10235-3"},{"key":"27_CR30","doi-asserted-by":"crossref","unstructured":"D.L.Musser, On proving inductive properties of abstract data types, Proc. 7th Conf., Las Vegas (1980)","DOI":"10.1145\/567446.567461"},{"key":"27_CR31","unstructured":"M.Nivat, Nondeterministic programs: an algebraic overview, Proc. of the IFIP 80 Conf., North-Holland Publishing Company (1980)."},{"key":"27_CR32","doi-asserted-by":"crossref","unstructured":"S.Porat, N.Francez, Fairness in term rewriting systems, Proc. 1st RTA Conf., Dijon (1985).","DOI":"10.1007\/3-540-15976-2_14"},{"key":"27_CR33","unstructured":"A.Poign\u00e9, On effective computations of nondeterministic schemes, Proc. of the CAAP-81 Conference, L.N.C.S. N.112 (1981)"},{"key":"27_CR34","unstructured":"J.L.Remy, H.Zhang, Contextual rewriting, Proc. 1st RTA Conf., Dijon (1985)"}],"container-title":["Lecture Notes in Computer Science","ESOP 86"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-16442-1_27.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:10:07Z","timestamp":1605643807000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-16442-1_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1986]]},"ISBN":["9783540164425","9783540397823"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/3-540-16442-1_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1986]]}}}