Bibliography

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

[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. Cited in 1.4.

[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. Cited in 13.5.1.

[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. Cited in 15.1.

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

[6]   Krzysztof R. Apt. Chapter 10 - Logic programming. In Jan Van Leeuwen, editor, Formal Models and Semantics, Handbook of Theoretical Computer Science, pages 493 – 574. Elsevier, Amsterdam, 1990. Cited in 15.6.

[7]   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. Cited in 15.1.

[8]   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. Cited in 13.5.2, 15.2, 15.7.

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

[10]   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. Cited in 1.1.2, 7.1.

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

[12]   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. Cited in 1.7, 3.

[13]   Peter Borovanský, Claude Kirchner, Hélène Kirchner, and Christophe Ringeissen. Rewriting with strategies in ELAN: A functional semantics. Int. J. Found. Comput. Sci., 12(1):69–95, 2001. Cited in 10.

[14]   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. Cited in 14.1.

[15]   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. Cited in 13.7.1.

[16]   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. Cited in 13.7, 13.7.1, 13.7.3.

[17]   Adel Bouhoula, Jean-Pierre Jouannaud, and José Meseguer. Specification and proof in membership equational logic. Theoretical Computer Science, 236:35–132, 2000. Cited in 1.2, 3.5, 4, 4.3, 4.6, 4.7, 6.1.1, 13.5.1.

[18]   Martin Bravenboer, Karl Trygve Kalleberg, Rob Vermaas, and Eelco Visser. Stratego/XT 0.17. A language and toolset for program transformation. Science of Computer Programming, 72(1-2):52–70, 2008. Cited in 10.

[19]   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. Cited in 1.2, 5.3, 6.1.1.

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

[21]   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. Cited in 6, 6.3, 21.3.1.

[22]   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. Cited in 1.5.

[23]   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. Cited in 13.5.1, 14.1.

[24]   Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking. MIT Press, 1999. Cited in 12, 12.3.

[25]   Manuel Clavel. Reflection in Rewriting Logic: Metalogical Foundations and Metaprogramming Applications. CSLI Publications, 2000. Cited in 17, 17.7.

[26]   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.illinois.edu/maude1/tutorial/. Cited in 17.7.

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

[28]   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. Cited in 17.1, 17.7.

[29]   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. Cited in 1.7, 1, 5.3, 9.4, 11.4, 12.5.

[30]   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.illinois.edu/papers/. Cited in 1.3, 1.4, 4.7, 6.1.1, 6.3.2.

[31]   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. Cited in 1.4.

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

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

[34]   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 [76], pages 91–107. http://www.sciencedirect.com/science/journal/15710661. Cited in 1.1.2, 17.

[35]   Alain Colmerauer, Henry Kanoui, and Michel van Caneghem. Étude et réalisation d’un système Prolog. techreport, Groupe d’Intelligence Artificielle, U.E.R. de Luminy, Université d’Aix-Marseille II, 1979. Cited in 10.5.

[36]   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. Cited in 13.5.1, 14.1, 14.7, 15.2.

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

[38]   Evelyne Contejean, Claude Marché, and Xavier Urbain. CiME, 2004. Available at http://cime.lri.fr/. Cited in 13.6, 13.7.

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

[40]   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. Cited in 4.8.

[41]   Arie van Deursen. Executable Language Definitions. PhD thesis, University of Amsterdam, 1994. Cited in 18.3.

[42]   Arie van Deursen, Jan Heering, and Paul Klint, editors. Language Prototyping: An Algebraic Specification Approach. World Scientific, 1996. Cited in 3, 10, 18.3.

[43]   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. Cited in 7.15.

[44]   Francisco Durán. A Reflective Module Algebra with Applications to the Maude Language. PhD thesis, University of Málaga, Spain, 1999. http://maude.cs.illinois.edu/papers/. Cited in 6, 21, 22.8.

[45]   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. Cited in 21.

[46]   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. Cited in 1.3, 4.7.

[47]   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. Cited in 1.3, 4.7, 21.5.

[48]   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/. Cited in 1.3.

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

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

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

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

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

[54]   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, volume 6381 of Lecture Notes in Computer Science, pages 69–85. Springer, 2010. Cited in 1.3, 4.7, 6.1.1, 13.5.3, 21.5.

[55]   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, volume 6381 of Lecture Notes in Computer Science, pages 86–103. Springer, 2010. Cited in 1.3, 13.5.3.

[56]   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. Cited in 1.3, 6.1.1, 13.5.3, 21.5.

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

[58]   Steven Eker. Term rewriting with operator evaluation strategies. In Kirchner and Kirchner [87], pages 311–330. http://www.sciencedirect.com/science/journal/15710661. Cited in 4.4.7, 17.

[59]   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. Cited in 1.1.3.

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

[61]   Steven Eker, Narciso Martí-Oliet, José Meseguer, and Alberto Verdejo. Deduction, strategies, and rewriting. In Myla Archer, Thierry Boy de la Tour, and César Muñoz, editors, Proceedings of the 6th International Workshop on Strategies in Automated Deduction, STRATEGIES 2006, Seattle, WA, USA, August 16, 2006, volume 174(11) of Electronic Notes in Theoretical Computer Science, pages 3–25. Elsevier, 2007. Cited in 10.

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

[63]   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. Cited in 15.8.

[64]   Santiago Escobar. Multi-paradigm programming in maude. In Vlad Rusu, editor, Rewriting Logic and Its Applications - 12th International Workshop, WRLA 2018, Held as a Satellite Event of ETAPS, Thessaloniki, Greece, June 14-15, 2018, Proceedings, volume 11152 of Lecture Notes in Computer Science, pages 26–44. Springer, 2018. Cited in 15.8.

[65]   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. Cited in 13.6.

[66]   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. Cited in 13.5.2.

[67]   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. Cited in 13.5.2.

[68]   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. Cited in 13.5.2, 15.2, 15.7.

[69]   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. Cited in 13.5.1, 14.1.

[70]   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. Cited in 13.5.1.

[71]   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. Cited in 13.5.1, 14.7, 15.2, 15.6, 15.7.

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

[73]   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. Cited in 15.1.

[74]   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. Cited in 27, 51.

[75]   Kokichi Futatsugi and Razvan Diaconescu. CafeOBJ Report. World Scientific, AMAST Series, 1998. Cited in 1.7.

[76]   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. Cited in 34, 62, 134.

[77]   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. Cited in 15.1.

[78]   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. Cited in 3.8, 4.

[79]   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. Cited in 2, 1.1.2, 1.7, 3.9.1, 3.9.2, 4.4.7, 6, 6.3, 21.3.1.

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

[81]   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. Cited in 4.4.7, 4.7.

[82]   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. Cited in 13.6.

[83]   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. Cited in 1.3, 4.7, 20.1.2.

[84]   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. Cited in 13.5.1, 14.7, 15.1, 15.3, 15.6.

[85]   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. Cited in 2, 13.5.1, 14.7, 15.3, 5.

[86]   Brian W. Kernighan and Dennis M. Ritchie. The C Programming Language, Second Edition. Prentice Hall, 1988. Cited in 3.1, 7.8, 24.3.

[87]   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. Cited in 49, 58.

[88]   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. Cited in 1.4.

[89]   Joop M. I. M. Leo. A general context-free parsing algorithm running in linear time on every LR(k) grammar without using lookahead. Theor. Comput. Sci., 82(1):165–176, 1991. Cited in 3.9.

[90]   Éduard Lucas. Recréations mathématiques. Albert Blanchard, 2 edition, 1992. Cited in 10.

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

[92]   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. Cited in 4.7.

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

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

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

[96]   Narciso Martí-Oliet, José Meseguer, and Alberto Verdejo. Towards a strategy language for Maude. In Narciso Martí-Oliet, editor, Proceedings of the Fifth International Workshop on Rewriting Logic and its Applications, WRLA 2004, Barcelona, Spain, March 27-April 4, 2004, volume 117 of Electronic Notes in Theoretical Computer Science, pages 417–441. Elsevier, 2004. Cited in 10.

[97]   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. Cited in 21.

[98]   Narciso Martí-Oliet, José Meseguer, and Alberto Verdejo. A rewriting semantics for Maude strategies. In Grigore Roc, u, editor, Proceedings of the Seventh 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 227–247. Elsevier, 2009. Cited in 10.

[99]   Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984. Cited in 7.5.

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

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

[102]   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. Cited in 15.1.

[103]   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. Cited in 22.1.4, 5.

[104]   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. Cited in 32, 57.

[105]   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. Cited in 1.2, 3.5, 4, 4.3, 4.7.

[106]   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. Cited in 2.

[107]   José Meseguer. Order-sorted rewriting and congruence closure. In Proc. FOSSACS 2016, volume 9634 of Lecture Notes in Computer Science, pages 493–509. Springer, 2016. Cited in 16.6.

[108]   José Meseguer. Variant-based satisfiability in initial algebras. Sci. Comput. Program., 154:3–41, 2018. Cited in 16.6.

[109]   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. Cited in 1.3.

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

[111]   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. Cited in 11.4.

[112]   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. Cited in 13.5.2, 15.1, 15.2, 15.3, 1, 15.4, 15.7.

[113]   Greg Nelson and Derek C. Oppen. Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst., 1(2):245–257, 1979. Cited in 16.6.

[114]   Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli. Solving SAT and SAT modulo theories: From an abstract davis–putnam–logemann–loveland procedure to dpll(T). Journal of the ACM, 53(6):937–977, 2006. Cited in 16.

[115]   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. Cited in 3.

[116]   Vivek Nigam, Carolyn Talcott, and Abraão Aires Urquiza. Towards the automated verification of cyber-physical security protocols: Bounding the number of timed intruders. In ESORICS 2016: European Symposium on Research in Computer Security, 2016. Cited in 17.6.12.

[117]   Vivek Nigam, Carolyn Talcott, and Abraão Aires Urquiza. Symbolic timed trace equivalence. In Foundations of Security, Protocols, and Equational Reasoning: Essays Dedicated to Catherine A. Meadows, LNCS, pages 89–111. Springer, 2019. Cited in 17.6.12.

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

[119]   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. Cited in 1.3, 1.4, 1.5.

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

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

[122]   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. Cited in 13.5.3.

[123]   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. Cited in 7.15.

[124]   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. Cited in 15.1.

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

[126]   C. Rocha and J. Meseguer. Five isomorphic boolean theories and four equational decision procedures. Technical Report UIUCDCS-R-2007-2818, CS Dept., University of Illinois at Urbana-Champaign, February 2007. Available at http://hdl.handle.net/2142/11295. Cited in 1.

[127]   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. Cited in 13.5.3.

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

[129]   Stephen Skeirik and José Meseguer. Metalevel algorithms for variant satisfiability. J. Log. Algebr. Meth. Program., 96:81–110, 2018. Cited in 16.6.

[130]   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. Cited in 13.6.

[131]   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. Cited in 13.7.1.

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

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

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

[135]   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. Cited in 13.5.1, 14.7, 21.5.

[136]   Patrick Viry. Equational rules for rewriting logic. Theoretical Computer Science, 285(2):487–517, 2002. Cited in 1.2, 5.3, 13.5.3.