TY - GEN
T1 - Unification and narrowing in maude 2.4
AU - Clavel, Manuel
AU - Durán, Francisco
AU - Eker, Steven
AU - Escobar, Santiago
AU - Lincoln, Patrick
AU - Martí-Oliet, Narciso
AU - Meseguer, José
AU - Talcott, Carolyn
N1 - Funding Information:
M. Clavel has been partially supported by MICINN grants TIN2005-09207-C03-03 and TIN2006-15660-C02-01, and by CAM program S-0505/TIC/0407. F. Durán has been partially supported by MICINN grant TIN2008-03107 and Junta de Andalucía P06-TIC2250 and P07-TIC3184. S. Escobar has been partially supported by MICINN grant TIN2007-68093-C02-02, Integrated Action HA 2006-0007, and Generalitat Valenciana GVPRE/2008/113. P. Lincoln’s effort partially supported by NSF grant CNS-0749931. N. Martí-Oliet has been partially supported by MICINN grant TIN2006-15660-C02-01 and CAM program S-0505/TIC/0407.
PY - 2009
Y1 - 2009
N2 - Maude is a high-performance reflective language and system supporting both equational and rewriting logic specification and programming for a wide range of applications, and has a relatively large worldwide user and open-source developer base. This paper introduces novel features of Maude 2.4 including support for unification and narrowing. Unification is supported in Core Maude, the core rewriting engine of Maude, with commands and metalevel functions for order-sorted unification modulo some frequently occurring equational axioms. Narrowing is currently supported in its Full Maude extension. We also give a brief summary of the most important features of Maude 2.4 that were not part of Maude 2.0 and earlier releases. These features include communication with external objects, a new implementation of its module algebra, and new predefined libraries. We also review some new Maude applications.
AB - Maude is a high-performance reflective language and system supporting both equational and rewriting logic specification and programming for a wide range of applications, and has a relatively large worldwide user and open-source developer base. This paper introduces novel features of Maude 2.4 including support for unification and narrowing. Unification is supported in Core Maude, the core rewriting engine of Maude, with commands and metalevel functions for order-sorted unification modulo some frequently occurring equational axioms. Narrowing is currently supported in its Full Maude extension. We also give a brief summary of the most important features of Maude 2.4 that were not part of Maude 2.0 and earlier releases. These features include communication with external objects, a new implementation of its module algebra, and new predefined libraries. We also review some new Maude applications.
UR - http://www.scopus.com/inward/record.url?scp=70349309222&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=70349309222&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-02348-4_27
DO - 10.1007/978-3-642-02348-4_27
M3 - Conference contribution
AN - SCOPUS:70349309222
SN - 3642023479
SN - 9783642023477
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 380
EP - 390
BT - Rewriting Techniques and Applications - 20th International Conference, RTA 2009, Proceedings
T2 - 20th International Conference on Rewriting Techniques and Applications, RTA 2009
Y2 - 29 June 2009 through 1 July 2009
ER -