×

Two decades of Maude. (English) Zbl 1321.68007

Martí-Oliet, Narciso (ed.) et al., Logic, rewriting, and concurrency. Essays dedicated to José Meseguer on the occasion of his 65th birthday. Cham: Springer (ISBN 978-3-319-23164-8/pbk; 978-3-319-23165-5/ebook). Lecture Notes in Computer Science 9200, 232-254 (2015).
Summary: This paper is a tribute to José Meseguer, from the rest of us in the Maude team, reviewing the past, the present, and the future of the language and system with which we have been working for around two decades under his leadership. After reviewing the origins and the language’s main features, we present the latest additions to the language and some features currently under development. This paper is not an introduction to Maude, and some familiarity with it and with rewriting logic are indeed assumed.
For the entire collection see [Zbl 1319.68011].

MSC:

68-03 History of computer science
01A65 Development of contemporary mathematics
03B70 Logic in computer science
68Q42 Grammars and rewriting systems
Full Text: DOI

References:

[1] Antoy, S.; Echahed, R.; Hanus, M., A needed narrowing strategy, J. ACM, 47, 4, 776-822 (2000) · Zbl 1327.68141 · doi:10.1145/347476.347484
[2] Bae, K., Escobar, S., Meseguer, J.: Abstract logical model checking of infinite-state systems using narrowing. In: van Raamsdonk, F. (ed.) 24th International Conference on Rewriting Techniques and Applications, RTA 2013, Eindhoven, The Netherlands, 24-26 June 2013. LIPIcs, vol. 21, pp. 81-96. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2013) · Zbl 1356.68140
[3] Bae, K.; Krisiloff, J.; Meseguer, J.; Ölveczky, PC, Designing and verifying distributed cyber-physical systems using multirate PALS: an airplane turning control system case study, Sci. Comput. Program., 103, 13-50 (2015) · doi:10.1016/j.scico.2014.09.011
[4] Bae, K.; Meseguer, J., Model checking linear temporal logic of rewriting formulas under localized fairness, Sci. Comput. Program., 99, 193-234 (2015) · doi:10.1016/j.scico.2014.02.006
[5] Barrett, C.; Conway, CL; Deters, M.; Hadarean, L.; Jovanović, D.; King, T.; Reynolds, A.; Tinelli, C.; Gopalakrishnan, G.; Qadeer, S., CVC4, Computer Aided Verification, 171-177 (2011), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-22110-1_14
[6] Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: Version 2.0. Technical report, Department of Computer Science, The University of Iowa (2010). http://smt-lib.org
[7] Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 825-885. IOS Press (2009) · Zbl 1183.68568
[8] Boronat, A.; Meseguer, J., An algebraic semantics for MOF, Formal Asp. Comput., 22, 3-4, 269-296 (2010) · Zbl 1213.68358 · doi:10.1007/s00165-009-0140-9
[9] Bouhoula, A.; Jouannaud, J-P; Meseguer, J., Specification and proof in membership equational logic, Theor. Comput. Sci., 236, 1, 35-132 (2000) · Zbl 0938.68057 · doi:10.1016/S0304-3975(99)00206-6
[10] Brands, S.; Chaum, D.; Helleseth, T., Distance bounding protocols, Advances in Cryptology - EUROCRYPT ’93, 344-359 (1994), Heidelberg: Springer, Heidelberg · Zbl 0951.94511 · doi:10.1007/3-540-48285-7_30
[11] Cerioli, M.; Meseguer, J., May i borrow your logic? (Transporting logical structure along maps), Theor. Comput. Sci., 173, 311-347 (1997) · Zbl 0901.68186 · doi:10.1016/S0304-3975(96)00160-0
[12] Clavel, M.: Reflection in General Logics and in Rewriting Logic, with Applications to the Maude Language. Ph.D. thesis, Universidad de Navarra, Spain, February 1998 · Zbl 0917.68108
[13] Clavel, M.: Reflection in general logics, rewriting logic, and Maude. In: Kirchner, Kirchner (eds.) [53], pp. 71-82 · Zbl 0917.68108
[14] Clavel, M.; Durán, F.; Eker, S.; Escobar, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Talcott, C.; Treinen, R., Unification and narrowing in Maude 2.4, Rewriting Techniques and Applications, 380-390 (2009), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-02348-4_27
[15] Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J.: Metalevel computation in Maude. In: Kirchner and Kirchner [53], pp. 331-352 · Zbl 0917.68024
[16] Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.F.: Maude: specification and programming in rewriting logic. SRI International, January 1999. http://maude.cs.uiuc.edu/maude1/manual/ · Zbl 0962.68108
[17] Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.F.: Maude as a metalanguage. In: Kirchner and Kirchner [53], pp. 147-160 · Zbl 0917.68106
[18] Clavel, M.; Durán, F.; Eker, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Quesada, JF; Narendran, P.; Rusinowitch, M., The Maude system, Rewriting Techniques and Applications, 240-243 (1999), Heidelberg: Springer, Heidelberg · doi:10.1007/3-540-48685-2_18
[19] Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.F.: A Maude tutorial. Tutorial distributed as documentation of the Maude system, Computer Science Laboratory, SRI International. Presented at the European Joint Conference on Theory and Practice of Software, ETAPS 2000, Berlin, Germany, 25 March 2000 · Zbl 0962.68108
[20] Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.F.: Towards Maude 2.0. In: Futatsugi [45], pp. 294-315
[21] Clavel, M.; Durán, F.; Eker, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Quesada, JF; Maibaum, T., Using Maude, Fundamental Approaches to Software Engineering, 371-374 (2000), Heidelberg: Springer, Heidelberg · doi:10.1007/3-540-46428-X_27
[22] Clavel, M.; Durán, F.; Eker, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Quesada, JF, Maude: specification and programming in rewriting logic, Theor. Comput. Sci., 285, 2, 187-243 (2002) · Zbl 1001.68059 · doi:10.1016/S0304-3975(01)00359-0
[23] Clavel, M.; Durán, F.; Eker, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Talcott, CL; Nieuwenhuis, R., The Maude 2.0 system, Rewriting Techniques and Applications, 76-87 (2003), Heidelberg: Springer, Heidelberg · Zbl 1038.68559 · doi:10.1007/3-540-44881-0_7
[24] Clavel, M.; Durán, F.; Eker, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Talcott, C., All About Maude - A High-Performance Logical Framework (2007), Heidelberg: Springer, Heidelberg · Zbl 1115.68046
[25] Clavel, M., Eker, S., Lincoln, P., Meseguer, J.: Principles of Maude. In: Meseguer [67], pp. 65-89 · Zbl 0912.68095
[26] Clavel, M., Meseguer, J.: Reflection and strategies in rewriting logic. In: Meseguer [67], pp. 126-148 · Zbl 0917.68107
[27] Comon-Lundh, H.; Delaune, S.; Giesl, J., The finite variant property: how to get rid of some algebraic properties, Term Rewriting and Applications, 294-307 (2005), Heidelberg: Springer, Heidelberg · Zbl 1078.68059 · doi:10.1007/978-3-540-32033-3_22
[28] Braga, CO; Haeusler, EH; Meseguer, J.; Mosses, PD; Rus, T., Maude action tool: using reflection to map action semantics to rewriting logic, Algebraic Methodology and Software Technology, 407-421 (2000), Heidelberg: Springer, Heidelberg · Zbl 0983.68519 · doi:10.1007/3-540-45499-3_29
[29] Durán, F.: A Reflective Module Algebra with Applications to the Maude Language. Ph.D. thesis, Universidad de Málaga, Spain, June 1999
[30] Durán, F.; Rus, T., The extensibility of Maude’s module algebra, Algebraic Methodology and Software Technology, 422-437 (2000), Heidelberg: Springer, Heidelberg · Zbl 0983.68522 · doi:10.1007/3-540-45499-3_30
[31] Durán, F., Eker, S., Escobar, S., Meseguer, J., Talcott, C.L.: Variants, unification, narrowing, and symbolic reachability in Maude 2.6. In: Schmidt-Schauß, M. (ed.) Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, RTA 2011, Novi Sad, Serbia, 30 May - 1 June, 2011. LIPIcs, vol. 10, pp. 31-40. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2011) · Zbl 1236.68180
[32] Durán, F.; Eker, S.; Lincoln, P.; Meseguer, J.; Kotz, D.; Mattern, F., Principles of mobile Maude, Agent Systems, Mobile Agents, and Applications, 73-85 (2000), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-540-45347-5_7
[33] Durán, F.; Lucas, S.; Meseguer, J.; Armando, A.; Baumgartner, P.; Dowek, G., MTT: the Maude termination tool (system description), Automated Reasoning, 313-319 (2008), Heidelberg: Springer, Heidelberg · Zbl 1165.68360 · doi:10.1007/978-3-540-71070-7_27
[34] Durán, F., Meseguer, J.: An extensible module algebra for Maude. In: Kirchner and Kirchner [53], pp. 174-195 · Zbl 0919.68076
[35] Durán, F.; Meseguer, J., Maude’s module algebra, Sci. Comput. Program., 66, 2, 125-153 (2007) · Zbl 1116.68047 · doi:10.1016/j.scico.2006.07.002
[36] Durán, F.; Meseguer, J., On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories, J. Logic Algebraic Program., 81, 7-8, 816-850 (2012) · Zbl 1272.03139 · doi:10.1016/j.jlap.2011.12.004
[37] Durán, F.; Riesco, A.; Verdejo, A., A distributed implementation of mobile Maude, Electr. Notes Theor. Comput. Sci., 176, 4, 113-131 (2007) · doi:10.1016/j.entcs.2007.06.011
[38] Durán, F.; Rocha, C.; Álvarez, JM; Agha, G.; Danvy, O.; Meseguer, J., Towards a Maude formal environment, Formal Modeling: Actors, Open Systems, Biological Systems, 329-351 (2011), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-24933-4_17
[39] Eker, S., Knapp, M., Laderoute, K., Lincoln, P., Meseguer, J., Sonmez, K.: Pathway logic: symbolic analysis of biological signaling. In: Proceedings of the Pacific Symposium on Biocomputing, pp. 400-412, January 2002
[40] Escobar, S.; Iida, S.; Meseguer, J.; Ogata, K., Functional logic programming in Maude, Specification, Algebra, and Software, 315-336 (2014), Heidelberg: Springer, Heidelberg · Zbl 1407.68081 · doi:10.1007/978-3-642-54624-2_16
[41] Escobar, S.; Meadows, C.; Meseguer, J.; Aldini, A.; Barthe, G.; Gorrieri, R., Maude-NPA: cryptographic protocol analysis modulo equational properties, Foundations of Security Analysis and Design V, 1-50 (2007), Heidelberg: Springer, Heidelberg · Zbl 1252.94061 · doi:10.1007/978-3-642-03829-7_1
[42] Escobar, S.; Meseguer, J.; Baader, F., Symbolic model checking of infinite-state systems using narrowing, Term Rewriting and Applications, 153-168 (2007), Heidelberg: Springer, Heidelberg · Zbl 1203.68097 · doi:10.1007/978-3-540-73449-9_13
[43] Escobar, S.; Sasse, R.; Meseguer, J., Folding variant narrowing and optimal variant termination, J. Logic Algebraic Program., 81, 7-8, 898-928 (2012) · Zbl 1291.68217 · doi:10.1016/j.jlap.2012.01.002
[44] Fadlisyah, M.; Ölveczky, PC; Ábrahám, E., Formal modeling and analysis of interacting hybrid systems in HI-Maude: what happened at the 2010 sauna world championships?, Sci. Comput. Program., 99, 95-127 (2015) · doi:10.1016/j.scico.2014.06.010
[45] Futatsugi, K. (ed.): Proceedings of the Third International Workshop on Rewriting Logic and its Applications, WRLA 2000, Kanazawa, Japan, 18-20 September 2000. Electronic Notes in Theoretical Computer Science. Elsevier, Amsterdam (2000) · Zbl 0957.00046
[46] Goguen, J., Meseguer, J.: Eqlog: equality, types and generic modules for logic programming. In: DeGroot, D., Lindstrom, G. (eds.) Logic Programming, Functions, Relations and Equations, pp. 295-363. Prentice-Hall (1986) · Zbl 0588.68005
[47] Goguen, J.; Meseguer, J., Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations, Theor. Comput. Sci., 105, 217-273 (1992) · Zbl 0778.68056 · doi:10.1016/0304-3975(92)90302-V
[48] Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.-P.: Introducing OBJ. In: Goguen, J.A., Malcolm, G. (eds.) Software Engineering with OBJ: Algebraic Specification in Action, pp. 3-167. Kluwer Academic Publishers (2000)
[49] Goguen, JA; Meseguer, J., Equality, types, modules, and (why not?) generics for logic programming, J. Logic Program., 1, 2, 179-210 (1984) · Zbl 0575.68091 · doi:10.1016/0743-1066(84)90004-9
[50] Hendrix, J.; Meseguer, J.; Ohsaki, H.; Furbach, U.; Shankar, N., A sufficient completeness checker for linear order-sorted specifications modulo axioms, Automated Reasoning, 151-155 (2006), Heidelberg: Springer, Heidelberg · doi:10.1007/11814771_14
[51] Kanovich, M., Kirigin, T.B., Nigam, V., Scedrov, A., Talcott, C., Perovic, R.: A rewriting framework for activities subject to regulations. In: Tiwari, A. (ed.) 23rd International Conference on RewritingTechniques and Applications (RTA). LIPIcs, vol. 15, pp. 305-322. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2012) · Zbl 1437.68082
[52] Kanovich, M.; Kirigin, TB; Nigam, V.; Scedrov, A.; Talcott, C.; Focardi, R.; Myers, A., Discrete vs. dense times in the analysis of cyber-physical security protocols, Principles of Security and Trust, 259-279 (2015), Heidelberg: Springer, Heidelberg
[53] Kirchner, C, Kirchner, H. (eds.) Proceedings of the Second International Workshop on Rewriting Logic and its Applications, WRLA 1998, Pont-à-Mousson, France, 1-4 September 1998. Electronic Notes in Theoretical Computer Science, vol. 15. Elsevier, Amsterdam (1998) · Zbl 0903.00070
[54] Lincoln, P., Martí-Oliet, N., Meseguer, J.: Specification, transformation, and programming of concurrent systems in rewriting logic. In: Blelloch, G.E., Chandy, K.M., Jagannathan, S. (eds.) Specification of Parallel Algorithms, DIMACS Workshop, 9-11 May 1994. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 18, pp. 309-339. American Mathematical Society (1994)
[55] Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Ricciulli, L.; Halatsis, C.; Philokyprou, G.; Maritsas, D.; Theodoridis, S., Compiling rewriting onto SIMD and MIMD/SIMD machines, PARLE ’94 Parallel Architectures and Languages Europe, 37-48 (1994), Heidelberg: Springer, Heidelberg · doi:10.1007/3-540-58184-7_88
[56] Lincoln, P.D., Talcott, C.: Symbolic systems biology and pathway logic. In: Iyengar, S. (eds.) Symbolic Systems Biology, pp. 1-29. Jones and Bartlett (2010)
[57] Lucas, S., Context-sensitive rewriting strategies, Inf. Comput., 178, 1, 294-343 (2002) · Zbl 1012.68095 · doi:10.1016/S0890-5401(02)93176-7
[58] Martí-Oliet, N., Meseguer, J.: Action and change in rewriting logic. In: Pareschi, R., Fronhöfer, B. (eds.) Dynamic Worlds: From the Frame Problem to Knowledge Management. Applied Logic Series, vol. 12, pp. 1-53. Kluwer Academic Publishers (1999) · Zbl 0930.03028
[59] Martí-Oliet, N., Meseguer, J.: Rewriting logic as a logical and semantic framework. In: Gabbay, D.M., Guenthner, F. (eds.) Handbook of Philosophical Logic, 2nd edn., vol. 9, pp. 1-87. Kluwer Academic Publishers (2002) · Zbl 0912.68096
[60] Martí-Oliet, N.; Palomino, M.; Verdejo, A., Rewriting logic bibliography by topic: 1990-2011, J. Logic Algebraic Program., 81, 7-8, 782-815 (2012) · Zbl 1262.03052 · doi:10.1016/j.jlap.2012.06.001
[61] Mason, I.A., Talcott, C.L.: IOP: the interoperability platform & IMaude: an interactive extension of Maude. In: Martí-Oliet, N. (ed.) Proceedings Fifth International Workshop on Rewriting Logic and its Applications, WRLA 2004, Barcelona, Spain, 27-28 March 2004. Electronic Notes in Theoretical Computer Science, vol. 117, pp. 315-333. Elsevier (2005). http://www.sciencedirect.com/science/journal/15710661
[62] Meseguer, J.: A logical theory of concurrent objects. In: Meyrowitz, N. (ed.) Proceedings of the ECOOP-OOPSLA 1990 Conference on Object-Oriented Programming, Ottawa, Canada, 21-25 October 1990, pp. 101-115. ACM Press (1990)
[63] Meseguer, J.; Baeten, JCM; Klop, JW, Rewriting as a unified model of concurrency, CONCUR 1990 Theories of Concurrency: Unification and Extension, 384-400 (1990), Heidelberg: Springer, Heidelberg · doi:10.1007/BFb0039072
[64] Meseguer, J., Conditional rewriting logic as a unified model of concurrency, Theor. Comput. Sci., 96, 1, 73-155 (1992) · Zbl 0758.68043 · doi:10.1016/0304-3975(92)90182-F
[65] Meseguer, J.; Kirchner, H.; Levi, G., Multiparadigm logic programming, Algebraic and Logic Programming, 158-200 (1992), Heidelberg: Springer, Heidelberg · doi:10.1007/BFb0013826
[66] Meseguer, J.: A logical theory of concurrent objects and its realization in the Maude language. In: Agha, G., Wegner, P., Yonezawa, A. (eds.) Research Directions in Concurrent Object-Oriented Programming, pp. 314-390. The MIT Press (1993)
[67] Meseguer, J. (ed.) Proceedings of the First International Workshop on Rewriting Logic and its Applications, WRLA 1996, Asilomar, California, 3-6 September 1996. Electronic Notes in Theoretical Computer Science, vol. 4. Elsevier, Amsterdam (1996) · Zbl 0903.00068
[68] Meseguer, J.; Sassone, V.; Montanari, U., Rewriting logic as a semantic framework for concurrency: a progressreport, CONCUR 1996: Concurrency Theory, 331-372 (1996), Heidelberg: Springer, Heidelberg · Zbl 1514.68175
[69] Meseguer, J.; Parisi-Presicce, F., Membership algebra as a logical framework for equationalspecification, Recent Trends in Algebraic Development Techniques, 18-61 (1998), Heidelberg: Springer, Heidelberg · Zbl 0903.08009 · doi:10.1007/3-540-64299-4_26
[70] Meseguer, J.; Futatsugi, K.; Jouannaud, J-P; Meseguer, J., From OBJ to Maude and beyond, Algebra, Meaning, and Computation, 252-280 (2006), Heidelberg: Springer, Heidelberg · Zbl 1132.68337 · doi:10.1007/11780274_14
[71] Meseguer, J.; Degano, P.; De Nicola, R.; Meseguer, J., The temporal logic of rewriting: a gentle introduction, Concurrency, Graphs and Models, 354-382 (2008), Heidelberg: Springer, Heidelberg · Zbl 1143.68459 · doi:10.1007/978-3-540-68679-8_22
[72] Meseguer, J., Twenty years of rewriting logic, J. Logic Algebraic Program., 81, 7-8, 721-781 (2012) · Zbl 1267.03043 · doi:10.1016/j.jlap.2012.06.003
[73] Meseguer, J.; Talcott, C.; Magnusson, B., Semantic models for distributed object reflection, ECOOP 2002 - Object-Oriented Programming, 1-36 (2002), Heidelberg: Springer, Heidelberg · Zbl 1049.68815 · doi:10.1007/3-540-47993-7_1
[74] Meseguer, J.; Thati, P., Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols, High.-Order Symbolic Comput., 20, 1-2, 123-160 (2007) · Zbl 1115.68079 · doi:10.1007/s10990-007-9000-6
[75] Meseguer, J.; Winkler, TC; Banâtre, J-P; Le Métayer, D., Parallel programmming in Maude, Research Directions in High-Level Parallel Programming Languages (1992), Heidelberg: Springer, Heidelberg
[76] Ölveczky, PC; Meseguer, J., Semantics and pragmatics of real-time Maude, High.-Order Symbolic Comput., 20, 1-2, 161-196 (2007) · Zbl 1115.68095 · doi:10.1007/s10990-007-9001-5
[77] Rivera, JE; Durán, F.; Vallecillo, A., Formal specification and analysis of domain specific models using Maude, Simulation, 85, 11-12, 778-792 (2009) · doi:10.1177/0037549709341635
[78] Rocha, C.; Meseguer, J.; Muñoz, C.; Escobar, S., Rewriting modulo SMT and open system analysis, Rewriting Logic and Its Applications, 247-262 (2014), Heidelberg: Springer, Heidelberg · Zbl 1367.68151
[79] Schmidt, K.; Nielsen, M.; Simpson, D., LoLA: a low level analyser, Application and Theory of Petri Nets 2000, 465-474 (2000), Heidelberg: Springer, Heidelberg · Zbl 0986.68684 · doi:10.1007/3-540-44988-4_27
[80] Talcott, C.: Symbolic modeling of signal transduction in pathway logic. In: Perrone, L.F., Wieland, F.P., Liu, J., Lawson, B.G., Nicol, D.M., Fujimoto, R.M. (eds.) 2006 Winter Simulation Conference, pp. 1656-1665 (2006)
[81] Talcott, C.; Dill, DL; Priami, C.; Plotkin, G., Multiple representations of biological processes, Transactions on Computational Systems Biology VI, 221-245 (2006), Heidelberg: Springer, Heidelberg · doi:10.1007/11880646_10
[82] Talcott, CL, Coordination models based on a formal model of distributed object reflection, Electr. Notes Theor. Comput. Sci., 150, 1, 143-157 (2006) · doi:10.1016/j.entcs.2005.12.028
[83] Winkler, TC; Lauer, PE, Programming in OBJ and Maude, Functional Programming, Concurrency, Simulation and Automated Reasoning, 229-277 (1993), Heidelberg: Springer, Heidelberg · doi:10.1007/3-540-56883-2_12
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.