Bibliography

[1]   Gul Agha. Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, 1986.

[2]   Gul Agha, José Meseguer, and Koushik Sen. PMaude: Rewrite-based specification language for probabilistic object systems. In A. Cerone and H. Wiklicky, editors, Proceedings Third Workshop on Quantitative Aspects of Programming Languages, QAPL’05, Edinburgh, UK, April 2005, volume 153(2) of Electronic Notes in Theoretical Computer Science, pages 213–239. Elsevier, 2006. http://www.sciencedirect.com/science/journal/15710661.

[3]   María Alpuente, Santiago Escobar, and José Iborra. Modular termination of basic narrowing. In Andrei Voronkov, editor, Rewriting Techniques and Applications, 19th International Conference, RTA 2008, Hagenberg, Austria, July 15-17, 2008, Proceedings, volume 5117 of Lecture Notes in Computer Science, pages 1–16. Springer, 2008.

[4]   María Alpuente, Moreno Falaschi, and Germán Vidal. Partial evaluation of functional logic programs. ACM Transactions on Programming Languages and Systems, 20(4):768–844, 1998.

[5]   María Alpuente, José Iborra, and Santiago Escobar. Termination of narrowing revisited. Theoretical Computer Science, 410(46):4608–4625, 2009.

[6]   Thomas Arts and Hans Zantema. Termination of logic programs using semantic unification. In Maurizio Proietti, editor, Logic Programming Synthesis and Transformation, 5th International Workshop, LOPSTR’95, Utrecht, The Netherlands, September 20-22, 1995, Proceedings, volume 1048 of Lecture Notes in Computer Science, pages 219–233. Springer, 1996.

[7]   Kyungmin Bae, Santiago Escobar, and José Meseguer. Abstract logical model checking of infinite-state systems using narrowing. In Femke van Raamsdonk, editor, 24th International Conference on Rewriting Techniques and Applications, RTA 2013, June 24-26, 2013, Eindhoven, The Netherlands, volume 21 of LIPIcs, pages 81–96. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2013.

[8]   David Basin, Manuel Clavel, and José Meseguer. Reflective metalogical frameworks. ACM Transactions on Computational Logic, 5(3):528–576, 2004.

[9]   Jan Bergstra and John Tucker. Characterization of computable data types by means of a finite equational specification method. In J. W. de Bakker and J. van Leeuwen, editors, Automata, Languages and Programming, 7th Colloquium, Noordweijkerhout, The Netherlands, July 14-18, 1980, Proceedings, volume 85 of Lecture Notes in Computer Science, pages 76–90. Springer, 1980.

[10]   Hans-Juergen Boehm, Russell R. Atkinson, and Michael F. Plass. Ropes: An alternative to strings. Software Practice and Experience, 25(12):1315–1330, 1995.

[11]   Peter Borovanský, Claude Kirchner, Hélčne Kirchner, and Pierre-Etienne Moreau. ELAN from a rewriting logic point of view. Theoretical Computer Science, 285(2):155–185, 2002.

[12]   Christopher Bouchard, Kimberly A. Gero, Christopher Lynch, and Paliath Narendran. On forward closure and the finite variant property. In Pascal Fontaine, Christophe Ringeissen, and Renate A. Schmidt, editors, Frontiers of Combining Systems - 9th International Symposium, FroCoS 2013, Nancy, France, September 18-20, 2013. Proceedings, volume 8152 of Lecture Notes in Computer Science, pages 327–342. Springer, 2013.

[13]   Alexandre Boudet. Unification in a combination of equational theories: an efficient algorithm. In Mark E. Stickel, editor, 10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 24-27, 1990, Proceedings, volume 449 of Lecture Notes in Computer Science, pages 292–307. Springer, 1990.

[14]   Alexandre Boudet, Evelyne Contejean, and Hervé Devie. A new AC-unification algorithm with an algorithm for solving systems of diophantine equations. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science (LICS 1990), pages 289–299. IEEE Computer Society Press, June 1990.

[15]   Adel Bouhoula, Jean-Pierre Jouannaud, and José Meseguer. Specification and proof in membership equational logic. Theoretical Computer Science, 236:35–132, 2000.

[16]   Roberto Bruni and José Meseguer. Generalized rewrite theories. In Jos C. M. Baeten, Jan Karel Lenstra, Joachim Parrow, and Gerhard J. Woeginger, editors, Automata, Languages and Programming, 30th International Colloquium, ICALP 2003, Eindhoven, The Netherlands, June 30 - July 4, 2003. Proceedings, volume 2719 of Lecture Notes in Computer Science, pages 252–266. Springer, 2003.

[17]   Randal E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 35(8):677–691, 1986.

[18]   Rod Burstall and Joseph A. Goguen. The semantics of Clear, a specification language. In Dines Bjřrner, editor, Abstract Software Specifications, 1979 Copenhagen Winter School, January 22 - February 2, 1979, Proceedings, volume 86 of Lecture Notes in Computer Science, pages 292–332. Springer, 1980.

[19]   Fabricio Chalub and Christiano Braga. Maude MSOS tool. In Grit Denker and Carolyn Talcott, editors, Proceedings Sixth International Workshop on Rewriting Logic and its Applications, WRLA 2006, Vienna, Austria, April 1–2, 2006, volume 176(4) of Electronic Notes in Theoretical Computer Science, pages 3–17. Elsevier, 2007. http://www.sciencedirect.com/science/journal/15710661.

[20]   Andrew Cholewa, José Meseguer, and Santiago Escobar. Variants of variants and the finite variant property. Technical report, Department of Computer Science, University of Illinois at Urbana-Champaign, http://hdl.handle.net/2142/47117, 2014.

[21]   Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking. MIT Press, 1999.

[22]   Manuel Clavel. Reflection in Rewriting Logic: Metalogical Foundations and Metaprogramming Applications. CSLI Publications, 2000.

[23]   Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and José F. Quesada. A tutorial on Maude. SRI International, March 2000, http://maude.cs.uiuc.edu/maude1/tutorial/.

[24]   Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and José F. Quesada. Towards Maude 2.0. In Futatsugi [68], pages 294–315. http://www.sciencedirect.com/science/journal/15710661.

[25]   Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and José F. Quesada. Maude: specification and programming in rewriting logic. Theoretical Computer Science, 285(2):187–243, 2002.

[26]   Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and Carolyn L. Talcott. All About Maude, A High-Performance Logical Framework, volume 4350 of Lecture Notes in Computer Science. Springer, 2007.

[27]   Manuel Clavel, Francisco Durán, Steven Eker, and José Meseguer. Building equational proving tools by reflection in rewriting logic. In Kokichi Futatsugi, Ataru T. Nakagawa, and Tetsuo Tamai, editors, CAFE: An Industrial-Strength Algebraic Formal Method. Elsevier, 2000. http://maude.cs.uiuc.edu/papers/.

[28]   Manuel Clavel, Francisco Durán, Steven Eker, José Meseguer, and Mark-Oliver Stehr. Maude as a formal meta-tool. In Jeannette M. Wing, Jim Woodcock, and Jim Davies, editors, FM’99 — Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 20–24, 1999 Proceedings, Volume II, volume 1709 of Lecture Notes in Computer Science, pages 1684–1703. Springer, 1999.

[29]   Manuel Clavel and José Meseguer. Reflection and strategies in rewriting logic. In Meseguer [94], pages 126–148. http://www.sciencedirect.com/science/journal/15710661.

[30]   Manuel Clavel and José Meseguer. Reflection in conditional rewriting logic. Theoretical Computer Science, 285(2):245–288, 2002.

[31]   Manuel Clavel, José Meseguer, and Miguel Palomino. Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic. In Gadducci and Montanari [70], pages 91–107. http://www.sciencedirect.com/science/journal/15710661.

[32]   Hubert Comon-Lundh and Stéphanie Delaune. The finite variant property: how to get rid of some algebraic properties. In Jürgen Giesl, editor, Term Rewriting and Applications, 16th International Conference, RTA 2005, Nara, Japan, April 19-21, 2005, Proceedings, volume 3467 of Lecture Notes in Computer Science, pages 294–307. Springer, 2005.

[33]   Evelyn Contejean and Hervé Devie. An efficient incremental algorithm for solving systems of linear diophantine equations. Information and Computation, 113(1):143–172, 1994.

[34]   Evelyne Contejean, Claude Marché, and Xavier Urbain. CiME, 2004. Available at http://cime.lri.fr/.

[35]   Nachum Dershowitz. Goal solving as operational semantics. In International Logic Programming Symposium, Portland, OR, pages 3–17. MIT Press, December 1995.

[36]   Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pages 243–320. North-Holland, 1990.

[37]   Arie van Deursen. Executable Language Definitions. PhD thesis, University of Amsterdam, 1994.

[38]   Arie van Deursen, Jan Heering, and Paul Klint, editors. Language Prototyping: An Algebraic Specification Approach. World Scientific, 1996.

[39]   Eric Domenjoud. Solving systems of linear diophantine equations: An algebraic approach. In Andrzej Tarlecki, editor, Mathematical Foundations of Computer Science 1991, 16th International Symposium, MFCS’91, Kazimierz Dolny, Poland, September 9-13, 1991, Proceedings, volume 520 of Lecture Notes in Computer Science, pages 141–150. Springer, 1991.

[40]    Francisco Durán. A Reflective Module Algebra with Applications to the Maude Language. PhD thesis, University of Málaga, Spain, 1999. http://maude.cs.uiuc.edu/papers/.

[41]   Francisco Durán. The extensibility of Maude’s module algebra. In Teodor Rus, editor, Algebraic Methodology and Software Technology, 8th International Conference, AMAST 2000, Iowa City, Iowa, USA, May 20-27, 2000, Proceedings, volume 1816 of Lecture Notes in Computer Science, pages 422–437. Springer, 2000.

[42]   Francisco Durán, Salvador Lucas, Claude Marché, José Meseguer, and Xavier Urbain. Proving operational termination of membership equational programs. Higher-Order and Symbolic Computation, 21(1-2):59–88, 2008.

[43]   Francisco Durán, Salvador Lucas, and José Meseguer. MTT: The Maude termination tool (system description). In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors, Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings, volume 5195 of Lecture Notes in Computer Science, pages 313–319. Springer, 2008.

[44]   Francisco Durán and José Meseguer. A Church-Rosser checker tool for Maude equational specifications. Manuscript, Computer Science Laboratory, SRI International, 2000. http://www.lcc.uma.es/~duran/CRC/.

[45]   Francisco Durán and José Meseguer. An extensible module algebra for Maude. In Kirchner and Kirchner [81], pages 174–195. http://www.sciencedirect.com/science/journal/15710661.

[46]   Francisco Durán and José Meseguer. The Maude specification of Full Maude. Technical report, Computer Science Laboratory, SRI International, February 1999. http://maude.cs.uiuc.edu/papers/.

[47]   Francisco Durán and José Meseguer. Parameterized theories and views in Full Maude 2.0. In Futatsugi [68], pages 316–338. http://www.sciencedirect.com/science/journal/15710661.

[48]   Francisco Durán and José Meseguer. Structured theories and institutions. Theoretical Computer Science, 309(1-3):357–380, 2003.

[49]   Francisco Durán and José Meseguer. Maude’s module algebra. Science of Computer Programming, 66(2):125–153, 2007.

[50]   Francisco Durán and José Meseguer. A Church-Rosser checker tool for conditional order-sorted equational Maude specifications. In Peter Csaba Ölveczky, editor, 8th International Workshop on Rewriting Logic and its Applications, WLRA 2010, Paphos, Cyprus, March 20-21, 2010, Proceedings, Lecture Notes in Computer Science. Springer, 2010. To appear.

[51]   Francisco Durán and José Meseguer. A Maude coherence checker tool for conditional order-sorted rewrite theories. In Peter Csaba Ölveczky, editor, 8th International Workshop on Rewriting Logic and its Applications, WLRA 2010, Paphos, Cyprus, March 20-21, 2010, Proceedings, Lecture Notes in Computer Science. Springer, 2010. To appear.

[52]   Francisco Durán and José Meseguer. On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories. Journal of Logic and Algebraic Programming, 81(7-8):816–850, 2012.

[53]   Steven Eker. Fast matching in combination of regular equational theories. In Meseguer [94], pages 90–109. http://www.sciencedirect.com/science/journal/15710661.

[54]   Steven Eker. Term rewriting with operator evaluation strategies. In Kirchner and Kirchner [81], pages 311–330. http://www.sciencedirect.com/science/journal/15710661.

[55]   Steven Eker. Associative-commutative rewriting on large terms. In Robert Nieuwenhuis, editor, Rewriting Techniques and Applications, 14th International Conference, RTA 2003, Valencia, Spain, June 9-11, 2003, Proceedings, volume 2706 of Lecture Notes in Computer Science, pages 14–29. Springer, 2003.

[56]   Steven Eker. Unification in Maude, January 2007. Talk at the “Protocol eXchange Seminar”, Naval Postgraduate School. Available at http://maude.cs.uiuc.edu/talks/eker-unification.pdf.

[57]   Steven Eker, José Meseguer, and Ambarish Sridharanarayanan. The Maude LTL model checker. In Gadducci and Montanari [70], pages 143–168. http://www.sciencedirect.com/science/journal/15710661.

[58]   Santiago Escobar. Functional logic programming in maude. In Shusaku Iida, José Meseguer, and Kazuhiro Ogata, editors, Specification, Algebra, and Software - Essays Dedicated to Kokichi Futatsugi, volume 8373 of Lecture Notes in Computer Science, pages 315–336. Springer, 2014.

[59]   Santiago Escobar, Joe Hendrix, Catherine Meadows, and José Meseguer. Diffie-Hellman cryptographic reasoning in the Maude-NRL protocol analyzer. In Monica Nesi and Ralf Treinen, editors, Proceedings Second International Workshop on Security and Rewriting Techniques, SecReT 2007, Paris, France, June 29, 2007, 2007.

[60]   Santiago Escobar, Catherine Meadows, and José Meseguer. A rewriting-based inference system for the NRL Protocol Analyzer and its meta-logical properties. Theoretical Computer Science, 367(1-2):162–202, 2006.

[61]   Santiago Escobar, Catherine Meadows, and José Meseguer. Maude-NPA: Cryptographic protocol analysis modulo equational properties. In Alessandro Aldini, Gilles Barthe, and Roberto Gorrieri, editors, Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures, volume 5705 of Lecture Notes in Computer Science, pages 1–50. Springer, 2009.

[62]   Santiago Escobar and José Meseguer. Symbolic model checking of infinite-state systems using narrowing. In Franz Baader, editor, Term Rewriting and Applications, 18th International Conference, RTA 2007, Paris, France, June 26-28, 2007, Proceedings, volume 4533 of Lecture Notes in Computer Science, pages 153–168. Springer, 2007.

[63]   Santiago Escobar, José Meseguer, and Ralf Sasse. Effectively checking the finite variant property. In Andrei Voronkov, editor, Rewriting Techniques and Applications, 19th International Conference, RTA 2008, Hagenberg, Austria, July 15-17, 2008, Proceedings, volume 5117 of Lecture Notes in Computer Science, pages 79–93. Springer, 2008.

[64]   Santiago Escobar, José Meseguer, and Ralf Sasse. Variant narrowing and equational unification. In Grigore Roşu, editor, Proceedings 7th International Workshop on Rewriting Logic and its Applications, WRLA 2008, Budapest, Hungary, March 29–30, 2008, volume 238(3) of Electronic Notes in Theoretical Computer Science, pages 88–102. Elsevier, 2009. http://www.sciencedirect.com/science/journal/15710661.

[65]   Santiago Escobar, Ralf Sasse, and José Meseguer. Folding variant narrowing and optimal variant termination. Journal of Logic and Algebraic Programming, 81(7-8):898–928, 2012.

[66]   François Fages. Associative-commutative unification. Journal of Symbolic Computation, 3(3):257–275, 1987.

[67]   M. Fay. First-order unification in an equational theory. In W. H. Joyner, editor, Proceedings of the 4th Workshop on Automated Deduction, Austin, Texas, USA, pages 161–167. Academic Press, 1979.

[68]   Kokichi Futatsugi, editor. Proceedings Third International Workshop on Rewriting Logic and its Applications, WRLA 2000, Kanazawa, Japan, September 18–20, 2000, volume 36 of Electronic Notes in Theoretical Computer Science. Elsevier, 2000. http://www.sciencedirect.com/science/journal/15710661.

[69]   Kokichi Futatsugi and Razvan Diaconescu. CafeOBJ Report. World Scientific, AMAST Series, 1998.

[70]   Fabio Gadducci and Ugo Montanari, editors. Proceedings Fourth International Workshop on Rewriting Logic and its Applications, WRLA 2002, Pisa, Italy, September 19–21, 2002, volume 71 of Electronic Notes in Theoretical Computer Science. Elsevier, 2004. http://www.sciencedirect.com/science/journal/15710661.

[71]   Joseph Goguen and José Meseguer. Eqlog: Equality, types and generic modules for logic programming. In Douglas DeGroot and Gary Lindstrom, editors, Logic Programming, Functions, Relations and Equations, pages 295–363. Prentice-Hall, 1986.

[72]   Joseph Goguen and José Meseguer. Order-sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoretical Computer Science, 105:217–273, 1992.

[73]   Joseph Goguen, Timothy Winkler, José Meseguer, Kokichi Futatsugi, and Jean-Pierre Jouannaud. Introducing OBJ. In Joseph A. Goguen and Grant Malcolm, editors, Software Engineering with OBJ: Algebraic Specification in Action, pages 3–167. Kluwer Academic Publishers, 2000.

[74]   Michael Hanus. The integration of functions into logic programming: From theory to practice. Journal of Logic Programming, 19&20:583–628, 1994.

[75]   Joe Hendrix and José Meseguer. On the completeness of context-sensitive order-sorted specifications. Technical Report UIUCDCS-R-2007-2812, Computer Science Dept., University of Illinois at Urbana-Champaign, February 2007.

[76]   Joe Hendrix and José Meseguer. Order-sorted equational unification revisited. In Günter Kniesel and Jorge Sousa Pinto, editors, Proceedings Ninth International Workshop on Rule-Based Programming, RULE 2008, Hagenberg Castle, Austria, volume 290 of Electronic Notes in Theoretical Computer Science, pages 37–50. Elsevier, 2012. http://www.sciencedirect.com/science/journal/15710661.

[77]   Joe Hendrix, José Meseguer, and Hitoshi Ohsaki. A sufficient completeness checker for linear order-sorted specifications modulo axioms. In Ulrich Furbach and Natarajan Shankar, editors, Automated Reasoning - Third International Joint Conference, IJCAR 2006, Seattle, Washington, August 17 - 20, 2006, Proceedings, volume 4130 of Lecture Notes in Artificial Intelligence, pages 151–155. Springer, 2006.

[78]   Jean-Marie Hullot. Canonical forms and unification. In Wolfgang Bibel and Robert A. Kowalski, editors, Fifth Conference on Automated Deduction, CADE 1980, Les Arcs, France, July 8-11, 1980, Proceedings, volume 87 of Lecture Notes in Computer Science, pages 318–334. Springer, 1980.

[79]   Jean-Pierre Jouannaud, Claude Kirchner, and Hélčne Kirchner. Incremental construction of unification algorithms in equational theories. In Josep Díaz, editor, Automata, Languages and Programming, 10th Colloquium, ICALP83, Barcelona, Spain, July 18-22, 1983, Proceedings, volume 154 of Lecture Notes in Computer Science, pages 361–373. Springer, 1983.

[80]   Brian W. Kernighan and Dennis M. Ritchie. The C Programming Language, Second Edition. Prentice Hall, 1988.

[81]   Claude Kirchner and Hélčne Kirchner, editors. Proceedings Second International Workshop on Rewriting Logic and its Applications, WRLA’98, Pont-ŕ-Mousson, France, September 1–4, 1998, volume 15 of Electronic Notes in Theoretical Computer Science. Elsevier, 1998. http://www.sciencedirect.com/science/journal/15710661.

[82]   Nirman Kumar, Koushik Sen, José Meseguer, and Gul Agha. A rewriting based model of probabilistic distributed object systems. In Elie Najm, Uwe Nestmann, and Perdita Stevens, editors, Formal Methods for Open Object-Based Distributed Systems: 6th IFIP WG 6.1 International Conference, FMOODS 2003, Paris, France, November 19.21, 2003. Proceedings, volume 2884 of Lecture Notes in Computer Science, pages 32–46. Springer, 2003.

[83]   Salvador Lucas. Context-sensitive computations in functional and functional logic programs. Journal of Functional and Logic Programming, 1998(1):1–61, 1998.

[84]   Salvador Lucas. Termination of rewriting with strategy annotations. In Robert Nieuwenhuis and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 8th International Conference, LPAR 2001, Havana, Cuba, December 3-7, 2001, Proceedings, volume 2250 of Lecture Notes in Artificial Intelligence, pages 669–684. Springer, 2001.

[85]   Salvador Lucas. Context-sensitive rewriting strategies. Information and Computation, 178(1):294–343, 2002.

[86]   Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems — Specification. Springer, 1992.

[87]   Alberto Martelli and Ugo Montanari. An efficient unification algorithm. ACM Transactions on Programming Languages and Systems, 4(2):258–282, 1982.

[88]   Narciso Martí-Oliet, José Meseguer, and Alberto Verdejo. Towards a strategy language for Maude. In Narciso Martí-Oliet, editor, Proceedings Fifth International Workshop on Rewriting Logic and its Applications, WRLA 2004, Barcelona, Spain, March 27–28, 2004, volume 117 of Electronic Notes in Theoretical Computer Science, pages 417–441. Elsevier, 2005. http://www.sciencedirect.com/science/journal/15710661.

[89]   Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984.

[90]   Ian A. Mason and Carolyn L. Talcott. Actor languages: Their syntax, semantics, translation, and equivalence. Theoretical Computer Science, 228(1), 1999.

[91]   José Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science, 96(1):73–155, 1992.

[92]   José Meseguer. Multiparadigm logic programming. In Hélčne Kirchner and Giorgio Levi, editors, Algebraic and Logic Programming, Third International Conference, Volterra, Italy, September 2–4, 1992, Proceedings, volume 632 of Lecture Notes in Computer Science, pages 158–200. Springer, 1992.

[93]   José Meseguer. A logical theory of concurrent objects and its realization in the Maude language. In Gul Agha, Peter Wegner, and Akinori Yonezawa, editors, Research Directions in Concurrent Object-Oriented Programming, pages 314–390. The MIT Press, 1993.

[94]   José Meseguer, editor. Proceedings First International Workshop on Rewriting Logic and its Applications, WRLA’96, Asilomar, California, September 3–6, 1996, volume 4 of Electronic Notes in Theoretical Computer Science. Elsevier, 1996. http://www.sciencedirect.com/science/journal/15710661.

[95]   José Meseguer. Membership algebra as a logical framework for equational specification. In Francesco Parisi-Presicce, editor, Recent Trends in Algebraic Development Techniques, 12th International Workshop, WADT’97, Tarquinia, Italy, June 3–7, 1997, Selected Papers, volume 1376 of Lecture Notes in Computer Science, pages 18–61. Springer, 1998.

[96]   José Meseguer. Strict coherence of conditional rewriting modulo axioms. Technical Report http://hdl.handle.net/2142/50288, Computer Science Department, University of Illinois at Urbana-Champaign, August 2014.

[97]   José Meseguer and Joseph Goguen. Initiality, induction and computability. In Maurice Nivat and John Reynolds, editors, Algebraic Methods in Semantics, pages 459–541. Cambridge University Press, 1985.

[98]   José Meseguer, Joseph A. Goguen, and Gert Smolka. Order-sorted unification. J. Symbolic Computation, 8(4):383–413, 1989.

[99]   José Meseguer, Miguel Palomino, and Narciso Martí-Oliet. Equational abstractions. In Franz Baader, editor, Automated Deduction - CADE-19. 19th International Conference on Automated Deduction, Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings, volume 2741 of Lecture Notes in Computer Science, pages 2–16. Springer, 2003.

[100]   José Meseguer and Prasanna Thati. Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols. Higher-Order and Symbolic Computation, 20(1-2):123–160, 2007.

[101]   Robert Nieuwenhuis and Albert Rubio. Paramodulation-based theorem proving. In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, pages 371–443. Elsevier and MIT Press, 2001.

[102]   Peter Csaba Ölveczky and José Meseguer. Specification of real-time and hybrid systems in rewriting logic. Theoretical Computer Science, 285(2):359–405, 2002.

[103]   Peter Csaba Ölveczky and José Meseguer. Specification and analysis of real-time systems using Real-Time Maude. In T. Margaria and M. Wermelinger, editors, Fundamental Approaches to Software Engineering, 7th International Conference, FASE 2004, Held as Part of ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings, volume 2984 of Lecture Notes in Computer Science, pages 354–358. Springer, 2004.

[104]   Peter Csaba Ölveczky and José Meseguer. Semantics and pragmatics of Real-Time Maude. Higher-Order and Symbolic Computation, 20(1-2):161–196, 2007.

[105]   Gerald E. Peterson and Mark E. Stickel. Complete sets of reductions for some equational theories. Journal of the ACM, 28(2):233–264, 1981.

[106]   Gordon Plotkin. Building-in equational theories. In Bernard Meltzer and Donald Michie, editors, Machine Intelligence 7, Proceedings of the Seventh Annual Machine Intelligence Workshop, Edinburgh, 1971, pages 73–90. Edinburgh University Press, 1972.

[107]   Loic Pottier. Minimal solutions of linear diophantine systems: bounds and algorithms. In Ronald V. Book, editor, Rewriting Techniques and Applications, 4th International Conference, RTA-91, Como, Italy, April 10-12, 1991, Proceedings, volume 488 of Lecture Notes in Computer Science, pages 162–173. Springer, 1991.

[108]   José F. Quesada. The SCP Parsing Algorithm Based on Syntactic Constraint Propagation. PhD thesis, Universidad de Sevilla, Spain, 1997.

[109]   José F. Quesada. The Maude parser: Parsing and meta-parsing β-extended context-free grammars. Technical Report, SRI International, Computer Science Laboratory, 1999.

[110]   Uday S. Reddy. Narrowing as the operational semantics of functional languages. In Proceedings of the 1985 Second Symposium on Logic Programming, Boston, Massachusetts, July 15-18, 1985, pages 138–151. IEEE Computer Society Press, 1985.

[111]   John Alan Robinson. A machine-oriented logic based on the resolution principle. Journal of the Association for Computing Machinery, 12(1):23–41, 1965.

[112]   Camilo Rocha and José Meseguer. Theorem proving modulo based on boolean equational procedures. In Rudolf Berghammer, Bernhard Möller, and Georg Struth, editors, Relations and Kleene Algebra in Computer Science, 10th International Conference on Relational Methods in Computer Science, and 5th International Conference on Applications of Kleene Algebra, RelMiCS/AKA 2008, Frauenwörth, Germany, April 7-11, 2008. Proceedings, volume 4988 of Lecture Notes in Computer Science, pages 337–351. Springer, 2008.

[113]   Manfred Schmidt-Schauss. Computational Aspects of Order-Sorted Logic with Term Declarations, volume 395 of Lecture Notes in Computer Science. Springer, 1989.

[114]   Gert Smolka, Werner Nutt, Joseph Goguen, and José Meseguer. Order-sorted equational computation. In Maurice Nivat and Hassan Aďt-Kaci, editors, Resolution of Equations in Algebraic Structures, volume 2, pages 297–367. Academic Press, 1989.

[115]   Mark E. Stickel. A complete unification algorithm for associative-commutative functions. In Advanced Papers of the Fourth International Joint Conference on Artificial Intelligence, Tbilisi, Georgia, USSR, 3-8 September 1975, pages 71–76, 1975.

[116]   Carolyn L. Talcott. Composable semantic models for actor theories. Higher-Order and Symbolic Computation, 11(3):281–343, 1998.

[117]   Ana Paula Tomás. On Solving Linear Diophantine Constraints. PhD thesis, Universidade do Porto, 1997.

[118]   Elena Tushkanova, Christophe Ringeissen, Alain Giorgetti, and Olga Kouchnarenko. Automatic decidability: A schematic calculus for theories with counting operators. In Femke van Raamsdonk, editor, 24th International Conference on Rewriting Techniques and Applications, RTA 2013, June 24-26, 2013, Eindhoven, The Netherlands, volume 21 of LIPIcs, pages 303–318. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2013.

[119]   Alberto Verdejo and Narciso Martí-Oliet. Implementing CCS in Maude 2. In Gadducci and Montanari [70], pages 263–281. http://www.sciencedirect.com/science/journal/15710661.

[120]   Emanuele Viola. E-unifiability via narrowing. In Antonio Restivo, Simona Ronchi Della Rocca, and Luca Roversi, editors, Theoretical Computer Science, 7th Italian Conference, ICTCS 2001, Torino, Italy, October 4-6, 2001, Proceedings, volume 2202 of Lecture Notes in Computer Science, pages 426–438. Springer, 2001.

[121]   Patrick Viry. Equational rules for rewriting logic. Theoretical Computer Science, 285(2):487–517, 2002.