[1] Gul Agha. Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, 1986. Cited in 162.
[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 20.
[3] 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 461.
[4] María Alpuente, José Iborra, and Santiago Escobar. Termination of narrowing revisited. Theoretical Computer Science, 410(46):4608–4625, 2009. Cited in 454, 466.
[5] 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 473.
[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. Cited in 461.
[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. Cited in 465, 476.
[8] David Basin, Manuel Clavel, and José Meseguer. Reflective metalogical frameworks. ACM Transactions on Computational Logic, 5(3):528–576, 2004. Cited in 21.
[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. Cited in 8, 244.
[10] Hans-Juergen Boehm, Russell R. Atkinson, and Michael F. Plass. Ropes: An alternative to strings. Softw. Pract. Exp., 25(12):1315–1330, 1995. Cited in 271.
[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. Cited in 24, 67.
[12] 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 359.
[13] 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 448.
[14] Adel Bouhoula, Jean-Pierre Jouannaud, and José Meseguer. Specification and proof in membership equational logic. Theoretical Computer Science, 236:35–132, 2000. Cited in 12, 14, 46, 63, 69, 98, 104, 179.
[15] 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 359.
[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. Cited in 12, 129, 130, 179.
[17] 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 175, 191.
[18] 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 448.
[19] Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking. MIT Press, 1999. Cited in 397, 409, 413, 421.
[20] Manuel Clavel. Reflection in Rewriting Logic: Metalogical Foundations and Metaprogramming Applications. CSLI Publications, 2000. Cited in 493, 549.
[21] 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, https://maude.cs.illinois.edu/maude1/tutorial/. Cited in 549.
[22] Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and José F. Quesada. Towards Maude 2.0. In 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, pages 294–315. Elsevier, 2000. http://www.sciencedirect.com/science/journal/15710661. Cited in 339.
[23] 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 495, 549.
[24] 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 23, 121, 128, 345, 391, 420.
[25] 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. https://maude.cs.illinois.edu/papers/. Cited in 18, 21, 107, 179, 199.
[26] 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 21.
[27] Manuel Clavel and José Meseguer. Reflection and strategies in rewriting logic. In Meseguer [94], pages 126–148. http://www.sciencedirect.com/science/journal/15710661. Cited in 493.
[28] Manuel Clavel and José Meseguer. Reflection in conditional rewriting logic. Theoretical Computer Science, 285(2):245–288, 2002. Cited in 10, 493.
[29] 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 [66], pages 91–107. http://www.sciencedirect.com/science/journal/15710661. Cited in 10, 493.
[30] 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 445, 447, 455, 464.
[31] 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 323, 324.
[32] Nachum Dershowitz. Goal solving as operational semantics. In International Logic Programming Symposium, Portland, OR, pages 3–17. MIT Press, December 1995. Cited in 461.
[33] 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 109.
[34] Arie van Deursen. Executable Language Definitions. PhD thesis, University of Amsterdam, 1994. Cited in 556.
[35] Arie van Deursen, Jan Heering, and Paul Klint, editors. Language Prototyping: An Algebraic Specification Approach. World Scientific, 1996. Cited in 67, 89, 556.
[36] 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 323.
[37] Francisco Durán. A Reflective Module Algebra with Applications to the Maude Language. PhD thesis, University of Málaga, Spain, 1999. https://maude.cs.illinois.edu/papers/. Cited in 172, 175.
[38] 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 18, 107, 391.
[39] 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 18, 107, 391.
[40] 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 18.
[41] Francisco Durán and José Meseguer. Structured theories and institutions. Theoretical Computer Science, 309(1-3):357–380, 2003. Cited in 175.
[42] Francisco Durán and José Meseguer. Maude’s module algebra. Science of Computer Programming, 66(2):125–153, 2007. Cited in 175.
[43] 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 18, 107, 179.
[44] 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 18.
[45] Francisco Durán and José Meseguer. On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories. J. Log. Algebraic Methods Program., 81(7-8):816–850, 2012. Cited in 18, 179, 392.
[46] Francisco Durán, José Meseguer, and Camilo Rocha. Ground confluence of order-sorted conditional specifications modulo axioms. J. Log. Algebraic Methods Program., 111:100513, 2020. Cited in 18, 392.
[47] Francisco Durán, Camilo Rocha, and José María Álvarez. Tool interoperability in the maude formal environment. In Andrea Corradini, Bartek Klin, and Corina Cîrstea, editors, Algebra and Coalgebra in Computer Science - 4th International Conference, CALCO 2011, Winchester, UK, August 30 - September 2, 2011. Proceedings, volume 6859 of Lecture Notes in Computer Science, pages 400–406. Springer, 2011. Cited in 18, 391, 392, 392.
[48] Francisco Durán, Camilo Rocha, and José María Álvarez. Towards a maude formal environment. In Gul Agha, Olivier Danvy, and José Meseguer, editors, Formal Modeling: Actors, Open Systems, Biological Systems - Essays Dedicated to Carolyn Talcott on the Occasion of Her 70th Birthday, volume 7000 of Lecture Notes in Computer Science, pages 329–351. Springer, 2011. Cited in 18, 391, 392, 392.
[49] Steven Eker. Fast matching in combination of regular equational theories. In Meseguer [94], pages 90–109. http://www.sciencedirect.com/science/journal/15710661. Cited in 11.
[50] Steven Eker. Term rewriting with operator evaluation strategies. In 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, pages 311–330. Elsevier, 1998. http://www.sciencedirect.com/science/journal/15710661. Cited in 81, 83, 116.
[51] 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 11.
[52] 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 359.
[53] Steven Eker, José Meseguer, and Ambarish Sridharanarayanan. The Maude LTL model checker. In Gadducci and Montanari [66], pages 143–168. http://www.sciencedirect.com/science/journal/15710661. Cited in 409, 418.
[54] Serdar Erbatur, Santiago Escobar, Deepak Kapur, Zhiqiang Liu, Christopher Lynch, Catherine A. Meadows, José Meseguer, Paliath Narendran, Sonia Santiago, and Ralf Sasse. Effective symbolic protocol analysis via equational irreducibility conditions. In Sara Foresti, Moti Yung, and Fabio Martinelli, editors, Computer Security - ESORICS 2012 - 17th European Symposium on Research in Computer Security, Pisa, Italy, September 10-12, 2012. Proceedings, volume 7459 of Lecture Notes in Computer Science, pages 73–90. Springer, 2012. Cited in 474.
[55] 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 481.
[56] 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 481.
[57] 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 474.
[58] 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 474.
[59] 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 465, 476.
[60] Santiago Escobar and José Meseguer. Canonical narrowing with irreducibility constraints as a symbolic protocol analysis method. In Joshua D. Guttman, Carl E. Landwehr, José Meseguer, and Dusko Pavlovic, editors, Foundations of Security, Protocols, and Equational Reasoning - Essays Dedicated to Catherine A. Meadows, volume 11565 of Lecture Notes in Computer Science, pages 15–38. Springer, 2019. Cited in 474.
[61] 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 447.
[62] 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 455, 464, 471, 476.
[63] F. J. Thayer Fabrega, J. Herzog, and J. Guttman. Strand Spaces: What makes a security protocol correct? Journal of Computer Security, 7:191–230, 1999. Cited in 474.
[64] 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 461.
[65] Kokichi Futatsugi and Razvan Diaconescu. CafeOBJ Report. World Scientific, AMAST Series, 1998. Cited in 24.
[66] 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 679, 682, 690.
[67] 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 461.
[68] 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 50, 63.
[69] 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 6, 9, 24, 53, 54, 81, 175, 191.
[70] Michael Hanus. The integration of functions into logic programming: From theory to practice. Journal of Logic Programming, 19&20:583–628, 1994. Cited in 461, 481.
[71] 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 83, 106, 107.
[72] Joe Hendrix and José Meseguer. On the completeness of context-sensitive order-sorted specifications. 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 229–245. Springer, 2007. Cited in 392.
[73] 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 18, 107, 613.
[74] 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 454, 461, 465, 471.
[75] 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 431, 454, 465, 466.
[76] D. Kapur and P. Narendran. Matching, Unification and Complexity. ACM SIGSAM Bulletin, 21(4):6–9, 1987. Cited in 456, 475.
[77] Brian W. Kernighan and Dennis M. Ritchie. The C Programming Language, Second Edition. Prentice Hall, 1988. Cited in 39, 271, 671.
[78] Dohan Kim, Christopher Lynch, and Paliath Narendran. Reviving basic narrowing modulo. In Andreas Herzig and Andrei Popescu, editors, Frontiers of Combining Systems - 12th International Symposium, FroCoS 2019, London, UK, September 4-6, 2019, Proceedings, volume 11715 of Lecture Notes in Computer Science, pages 313–329. Springer, 2019. Cited in 455.
[79] 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 20.
[80] 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 51.
[81] Éduard Lucas. Recréations mathématiques. Albert Blanchard, 2 edition, 1992. Cited in 359.
[82] Salvador Lucas. Context-sensitive computations in functional and functional logic programs. Journal of Functional and Logic Programming, 1998(1):1–61, 1998. Cited in 107, 469.
[83] 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 107.
[84] Salvador Lucas. Context-sensitive rewriting strategies. Information and Computation, 178(1):294–343, 2002. Cited in 107.
[85] Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems — Specification. Springer, 1992. Cited in 397.
[86] 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 359.
[87] Narciso Martí-Oliet, José Meseguer, and Alberto Verdejo. A rewriting semantics for Maude strategies. In Grigore Ro
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 359.
[88] Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984. Cited in 263.
[89] Ian A. Mason and Carolyn L. Talcott. Actor languages: Their syntax, semantics, translation, and equivalence. Theoretical Computer Science, 228(1), 1999. Cited in 156.
[90] Makoto Matsumoto and Takuji Nishimura. Mersenne twister: A 623-dimensionally equidistributed uniform pseudo-random number generator. ACM Trans. Model. Comput. Simul., 8(1):3–30, 1998. Cited in 255.
[91] José Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science, 96(1):73–155, 1992. Cited in 12, 130.
[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. Cited in 461.
[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. Cited in 146, 169.
[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. Cited in 678, 681.
[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. Cited in 12, 46, 63, 69, 99.
[96] José Meseguer. Strict coherence of conditional rewriting modulo axioms. Theor. Comput. Sci., 672:1–35, 2017. Cited in 431, 448, 450.
[97] José Meseguer. Generalized rewrite theories, coherence completion, and symbolic methods. J. Log. Algebraic Methods Program., 110, 2020. Cited in 448, 450, 468.
[98] 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 17.
[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. Cited in 391.
[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. Cited in 428, 461, 464, 465, 466, 468, 475.
[101] 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 487.
[102] 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 462.
[103] 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 532.
[104] 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 532.
[105] 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 147, 152.
[106] 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 18, 20.
[107] 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 18, 20, 147, 152.
[108] 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 324.
[109] 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 461.
[110] 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 486.
[111] Rubén Rubio, Narciso Martí-Oliet, Isabel Pita, and Alberto Verdejo. Metalevel transformation of strategies. J. Log. Algebr. Methods Program., 124, 2022. Cited in 550.
[112] Carolyn L. Talcott. Composable semantic models for actor theories. Higher-Order and Symbolic Computation, 11(3):281–343, 1998. Cited in 162.
[113] Ana Paula Tomás. On Solving Linear Diophantine Constraints. PhD thesis, Universidade do Porto, 1997. Cited in 323.
[114] Alberto Verdejo and Narciso Martí-Oliet. Implementing CCS in Maude 2. In Gadducci and Montanari [66], pages 263–281. http://www.sciencedirect.com/science/journal/15710661. Cited in 122.
[115] 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 455.
[116] Patrick Viry. Equational rules for rewriting logic. Theoretical Computer Science, 285(2):487–517, 2002. Cited in 14, 15, 125, 128.