A rewriting logic approach to operational semantics.(English)Zbl 1165.68041

Summary: This paper shows how Rewriting Logic Semantics (RLS) can be used as a computational logic framework for operational semantic definitions of programming languages. Several operational semantics styles are addressed: big-step and small-step Structural Operational Semantics (SOS), modular SOS, reduction semantics with evaluation contexts, continuation-based semantics, and the chemical abstract machine. Each of these language definitional styles can be faithfully captured as an RLS theory, in the sense that there is a one-to-one correspondence between computational steps in the original language definition and computational steps in the corresponding RLS theory. A major goal of this paper is to show that RLS does not force or pre-impose any given language definitional style, and that its flexibility and ease of use makes RLS an appealing framework for exploring new definitional styles.

MSC:

 68Q55 Semantics in the theory of computing 03B70 Logic in computer science 68Q42 Grammars and rewriting systems
Full Text:

References:

 [1] M. Abadi, L. Cardelli, P.-L. Curien, J.-J. Lévy, Explicit substitutions, in: POPL ’90: Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM Press, New York, NY, USA, 1990, pp. 31-46. · Zbl 0941.68542 [2] G.A. Agha, J. Meseguer, K. Sen, PMaude: rewrite-based specification language for probabilistic object systems, in: 3rd Workshop on Quantitative Aspects of Programming Languages (QAPL 05), Electronic Notes in Theoretical Computer Science, vol. 153, No. 2, 2006, pp. 213-239. [3] W. Ahrendt, A. Roth, R. Sasse, Automatic validation of transformation rules for java verification against a rewriting semantics, in: G. Sutcliffe, A. Voronkov (Eds.), Logic for Programming, Artificial Intelligence, and Reasoning, 12th International Conference, LPAR 2005, Montego Bay, Jamaica, December 2-6, 2005, Proceedings, Lecture Notes in Computer Science, vol. 3835, Springer, 2005, pp. 412-426. · Zbl 1143.68348 [4] M. Al-Turki, A Rewriting Logic Approach to the Semantics of Orc, Master’s thesis, Department of Computer Science, University of Illinois at Urbana-Champaign, December 2005. [5] M. AlTurki, J. Meseguer, Real-time rewriting semantics of orc, in: M. Leuschel, A. Podelski (Eds.), Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 14-16, 2007, ACM Press, Wroclaw, Poland, 2007, pp. 131-142. [6] Banâtre, J.-P.; Métayer, D.L., The GAMMA model and its discipline of programming, Science of computer programming, 15, 1, 55-77, (1990) · Zbl 0715.68054 [7] Benaissa, Z.-E.-A.; Briaud, D.; Lescanne, P.; Rouyer-Degli, J., $$\lambda - \nu$$, a calculus of explicit substitutions which preserves strong normalisation, The journal of functional programming, 6, 5, 699-722, (1996) · Zbl 0873.68108 [8] Berry, G.; Boudol, G., The chemical abstract machine, Theoretical computer science, 96, 1, 217-248, (1992) · Zbl 0747.68013 [9] P. Borovanský, H. Cirstea, H. Dubois, C. Kirchner, H. Kirchner, P.-E. Moreau, C. Ringeissen, M. Vittek, ELAN V 3.4 User Manual, LORIA, Nancy (France), fourth ed., January 2000. [10] Borovanský, P.; Kirchner, C.; Kirchner, H.; Moreau, P.-E., ELAN from a rewriting logic point of view, Theoretical computer science, 285, 2, 155-185, (2002) · Zbl 1001.68057 [11] P. Borras, D. Clément, T. Despeyroux, J. Incerpi, G. Kahn, B. Lang, V. Pascual, CENTAUR: the system, in: Software Development Environments (SDE), 1988, pp. 14-24. [12] C. Braga, Rewriting Logic as a Semantic Framework for Modular Structural Operational Semantics, Ph.D. thesis, Departamento de Informática, Pontificia Universidade Católica de Rio de Janeiro, Brasil, 2001. [13] C. Braga, J. Meseguer, Modular rewriting semantics in practice, in: Proceedings of the Fifth International Workshop on Rewriting Logic and its Applications (WRLA 2004), Electronic Notes in Theoretical Computer Science, vol. 117, Elsevier, 2005, pp. 393-416. · Zbl 1272.68168 [14] Broy, M.; Wirsing, M.; Pepper, P., On the algebraic definition of programming languages, ACM transactions on programming languages and systems (TOPLAS), 9, 1, 54-99, (1987) · Zbl 0627.68009 [15] Bruni, R.; Meseguer, J., Semantic foundations for generalized rewrite theories, Theoretical computer science, 360, 1-3, 386-414, (2006) · Zbl 1097.68051 [16] I. Cervesato, M.-O. Stehr, Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types, in: P. Degano (Ed.), Proceedings of the Fifth International Workshop on Rewriting Logic and its Applications (WRLA 2004), Electronic Notes in Theoretical Computer Science, vol. 117, Elsevier, 2005, pp. 183-207. · Zbl 1272.68171 [17] F. Chalub, An Implementation of Modular SOS in Maude, Master’s thesis, Universidade Federal Fluminense, May 2005. Available from: . [18] Chalub, F.; Braga, C., A modular rewriting semantics for CML, The journal of universal computer science, 10, 7, 789-807, (2004) [19] F. Chalub, C. Braga, Maude MSOS tool, in: G. Denker, C. Talcott (Eds.), Proceedings of the Sixth International Workshop on Rewriting Logic and its Applications (WRLA 2006), Electronic Notes in Theoretical Computer Science, vol. 176, No. 4, Elsevier, 2007, pp. 133-146. [20] F. Chen, G. Roşu, Rewriting Logic Semantics of Java 1.4, 2004. Available from: , Rewriting_Logic_Semantics_of_Java. [21] F. Chen, G. Rosu, R.P. Venkatesan, Rule-based analysis of dimensional safety, in: R. Nieuwenhuis (Ed.), Rewriting Techniques and Applications, 14th International Conference, RTA 2003, Valencia, Spain, June 9-11, 2003, Proceedings, Lecture Notes in Computer Science, vol. 2706, Springer, 2003, pp. 197-207. · Zbl 1038.68548 [22] Clavel, M.; Durán, F.; Eker, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Quesada, J.F., Maude: specification and programming in rewriting logic, Theoretical computer science, 285, 2, 187-243, (2002) · Zbl 1001.68059 [23] M. Clavel, F. Durán, S. Eker, J. Meseguer, P. Lincoln, N. Martí-Oliet, C. Talcott, All about Maude, A High-Performance Logical Framework, Lecture Notes in Computer Science, vol. 4350, Springer, 2007. · Zbl 1115.68046 [24] M. Clavel, J. Santa-Cruz, ASIP+ITP: a verification tool based on algebraic semantics, in: PROLE 2005: V Jornadas sobre Programacin y Lenguajes, Thomson, 2005, pp. 149-158. [25] D. Clément, J. Despeyroux, L. Hascoet, G. Kahn, Natural semantics on the computer, in: K. Fuchi, M. Nivat (Eds.), Proceedings of the France-Japan AI and CS Symposium, ICOT, Japan, 1986, pp. 49-89, Also, Information Processing Society of Japan, Technical Memorandum PL-86-6 and Rapport de recherche #0416, INRIA. [26] M. d’Amorim, G. Rosu, An equational specification for the Scheme language, The Journal of Universal Computer Science, 11 (7) (2005) 1327-1348, Selected papers from the 9th Brazilian Symposium on Programming Languages (SBLP’05), Also Technical Report No. UIUCDCS-R-2005-2567, April 2005. [27] O. Danvy, L.R. Nielsen. Refocusing in reduction semantics, RS RS-04-26, BRICS, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, November 2004, This report supersedes BRICS report RS-02-04, A preliminary version appears in the informal proceedings of the Second International Workshop on Rule-Based Programming, RULE 2001, Electronic Notes in Theoretical Computer Science, vol. 59.4. [28] R. Diaconescu, K. Futatsugi, CafeOBJ Report, The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification, AMAST Series in Computing, vol. 6, World Scientific, 1998. [29] S. Eker, N. Martí-Oliet, J. Meseguer, A. Verdejo, Deduction, strategies, and rewriting, in: T. Boy de la Tour, M. Archer, C. Muoz (Eds.), Proceedings of the 6th International Workshop on Strategies in Automated Deduction (STRATEGIES 2006), Electronic Notes in Theoretical Computer Science, vol. 174, No. 11, Elsevier, 2007, pp. 3-25. · Zbl 1277.68241 [30] A. Farzan, Static and Dynamic Formal Analysis of Concurrent Systems and Languages: A Semantics-based Approach, Ph.D. thesis, Department of Computer Science, University of Illinois at Urbana-Champaign, 2007. [31] A. Farzan, F. Chen, J. Meseguer, G. Rosu, Formal analysis of Java programs in JavaFAN, in: R. Alur, D. Peled (Eds.), Computer Aided Verification, 16th International Conference, CAV 2004, Boston, MA, USA, July 13-17, 2004, Proceedings, Lecture Notes in Computer Science, vol. 3114, Springer, 2004, pp. 501-505. · Zbl 1103.68611 [32] A. Farzan, J. Meseguer, Partial order reduction for rewriting semantics of programming languages, in: G. Denker, C. Talcott (Eds.), Proceedings of the Sixth International Workshop on Rewriting Logic and its Applications (WRLA 2006), Electronic Notes in Theoretical Computer Science, vol. 176, No. 4, Elsevier, 2007, pp. 61-78. · Zbl 1279.68207 [33] A. Farzan, J. Meseguer, G. Rosu, Formal JVM code analysis in JavaFAN, in: C. Rattray, S. Maharaj, C. Shankland (Eds.), Algebraic Methodology and Software Technology, 10th International Conference, AMAST 2004, Stirling, Scotland, UK, July 12-16, 2004, Proceedings, Lecture Notes in Computer Science, vol. 3116, Springer, 2004, pp. 132-147. · Zbl 1108.68382 [34] M. Felleisen, D.P. Friedman, Control operators, the SECD-machine, and the lambda-calculus, in: 3rd Working Conference on the Formal Description of Programming Concepts, Ebberup, Denmark, August 1986, pp. 193-219. [35] Friedman, D.P.; Wand, M.; Haynes, C.T., Essentials of programming languages, (2001), MIT Press Cambridge, MA · Zbl 0994.68020 [36] A. Garrido, J. Meseguer, R. Johnson, Algebraic Semantics of the C Preprocessor and Correctness of its Refactorings, Technical Report UIUCDCS-R-2006-2688, Department of Computer Science, University of Illinois at Urbana-Champaign, February 2006. [37] Goguen, J.; Malcolm, G., Algebraic semantics of imperative programs, (1996), MIT Press · Zbl 0887.68066 [38] J. Goguen, T. Winkler, J. Meseguer, K. Futatsugi, J.-P. Jouannaud, Introducing OBJ, in: J. Goguen (Ed.), Applications of Algebraic Specification using OBJ, Cambridge, 1993. [39] J.A. Goguen, K. Parsaye-Ghomi, Algebraic denotational semantics using parameterized abstract modules, in: J. Díaz, I. Ramos (Eds.), Formalization of Programming Concepts, International Colloquium, Peniscola, Spain, April 19-25, 1981, Proceedings, Lecture Notes in Computer Science, vol. 107, Springer, 1981, pp. 292-309. · Zbl 0467.68014 [40] Gurevich, Y., Evolving algebras 1993: lipari guide, (), 9-37 · Zbl 0852.68053 [41] Harper, R.; Honsell, F.; Plotkin, G.D., A framework for defining logics, Journal of the ACM, 40, 1, 143-184, (1993) · Zbl 0778.03004 [42] M. Hills, T.F. Şerbănuţă, G. Roşu, A rewrite framework for language definitions and for generation of efficient interpreters, in: G. Denker, C. Talcott (Eds.), Proceedings of the Sixth International Workshop on Rewriting Logic and its Applications (WRLA 2006), Electronic Notes in Theoretical Computer Science, vol. 176, No. 4, Elsevier, 2007, pp. 215-231. [43] E.B. Johnsen, O. Owe, E.W. Axelsen, A run-time environment for concurrent objects with asynchronous method calls, in: N. Martí-Oliet (Ed.), Proceedings of the Fifth International Workshop on Rewriting Logic and its Applications (WRLA 2004), Electronic Notes in Theoretical Computer Science, vol. 117, Elsevier, 2005, pp. 375-392. · Zbl 1272.68186 [44] G. Kahn, Natural semantics, in: F.-J. Brandenburg, G. Vidal-Naquet, M. Wirsing (Eds.), STACS 87, 4th Annual Symposium on Theoretical Aspects of Computer Science, Passau, Germany, February 19-21, 1987, Proceedings, Lecture Notes in Computer Science, vol. 247, Springer, 1987, pp. 22-39. · Zbl 0635.68007 [45] M. Katelman, J. Meseguer, A rewriting semantics for ABEL with applications to hardware/software co-design and analysis, in: G. Denker, C. Talcott (Eds.), Proceedings of the Sixth International Workshop on Rewriting Logic and its Applications (WRLA 2006), Electronic Notes in Theoretical Computer Science, vol. 176, No. 4, Elsevier, 2007, pp. 47-60. · Zbl 1279.68189 [46] Kaufmann, M.; Manolios, P.; Moore, J.S., Computer-aided reasoning: ACL2 case studies, (2000), Kluwer Academic Press [47] S. Liang, P. Hudak, M. Jones, Monad transformers and modular interpreters, in: POPL ’95: Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM Press, New York, NY, USA, 1995, pp. 333-343. [48] N. Martí-Oliet, J. Meseguer, Rewriting logic as a logical and semantic framework, in: D. Gabbay, F. Guenthner (Eds.), Handbook of Philosophical Logic, second ed., Kluwer Academic Publishers, 2002, pp. 1-87, First published as SRI Technical Report SRI-CSL-93-05, August 1993. · Zbl 0912.68096 [49] Martí-Oliet, N.; Meseguer, J., Rewriting logic: roadmap and bibliography, Theoretical computer science, 285, 2, 121-154, (2002) · Zbl 1027.68613 [50] Meseguer, J., Conditional rewriting logic as a unified model of concurrency, Theoretical computer science, 96, 1, 73-155, (1992) · Zbl 0758.68043 [51] J. Meseguer, Rewriting logic as a semantic framework for concurrency: a progress report, in: U. Montanari, V. Sassone (Eds.), CONCUR ’96, Concurrency Theory, 7th International Conference, Pisa, Italy, August 26-29, 1996, Proceedings, Lecture Notes in Computer Science, vol. 1119, Springer, 1996, pp. 331-372. [52] J. Meseguer, Membership algebra as a logical framework for equational specification, in: F. Parisi-Presicce (Ed.), Recent Trends in Algebraic Development Techniques, 12th International Workshop, WADT’97, Tarquinia, Italy, June 1997, Selected Papers, Lecture Notes in Computer Science, vol. 1376, Springer, 1997, pp. 18-61. · Zbl 0903.08009 [53] J. Meseguer, Software specification and verification in rewriting logic, in: M. Broy, M. Pizka (Eds.), Models, Algebras, and Logic of Engineering Software, NATO Advanced Study Institute, Marktoberdorf, Germany, July 30-August 11, 2002, IOS Press, 2003, pp. 133-193. [54] J. Meseguer, A rewriting logic sampler, in: D.V. Hung, M. Wirsing (Eds.), Theoretical Aspects of Computing—ICTAC 2005, Second International Colloquium, Hanoi, Vietnam, October 17-21, 2005, Proceedings, Lecture Notes in Computer Science, vol. 3722, Springer, 2005, pp. 1-28. · Zbl 1169.03349 [55] J. Meseguer, C. Braga, Modular rewriting semantics of programming languages, in: C. Rattray, S. Maharaj, C. Shankland (Eds.), Algebraic Methodology and Software Technology, 10th International Conference, AMAST 2004, Stirling, Scotland, UK, July 12-16, 2004, Proceedings, Lecture Notes in Computer Science, vol. 3116, Springer, 2004, pp. 364-378. · Zbl 1108.68401 [56] J. Meseguer, G. Rosu, Rewriting logic semantics: from language specifications to formal analysis tools, in: D.A. Basin, M. Rusinowitch (Eds.), Automated Reasoning—Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings, Lecture Notes in Computer Science, vol. 3097, Springer, 2004, pp. 1-44. · Zbl 1126.68464 [57] Meseguer, J.; Rosu, G., The rewriting logic semantics project, Theoretical computer science, 373, 3, 213-237, (2007) · Zbl 1111.68068 [58] D. Miller, Representing and reasoning with operational semantics, in: U. Furbach, N. Shankar (Eds.), Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, Lecture Notes in Computer Science, vol. 4130, Springer, 2006, pp. 4-20. · Zbl 1222.68113 [59] Milner, R., Functions as processes, Mathematical structures in computer science, 2, 2, 119-141, (1992) · Zbl 0773.03012 [60] Milner, R.; Tofte, M.; Harper, R.; MacQueen, D., The definition of standard ML (revised), (1997), MIT Press [61] E. Moggi, An Abstract View of Programming Languages, Technical Report ECS-LFCS-90-113, Edinburgh University, Department of Computer Science, June 1989. [62] P.D. Mosses, Unified algebras and action semantics, in: B. Monien, R. Cori (Eds.), STACS 89, 6th Annual Symposium on Theoretical Aspects of Computer Science, Paderborn, FRG, February 16-18, 1989, Proceedings, Lecture Notes in Computer Science, vol. 349, Springer, 1989, pp. 17-35. [63] Mosses, P.D., Denotational semantics, (), (Chapter 11) · Zbl 0338.68021 [64] P.D. Mosses, Pragmatics of modular SOS, in: H. Kirchner, C. Ringeissen (Eds.), Algebraic Methodology and Software Technology, 9th International Conference, AMAST 2002, Saint-Gilles-les-Bains, Reunion Island, France, September 9-13, 2002, Proceedings, Lecture Notes in Computer Science, vol. 2422, Springer, 2002, pp. 21-40. · Zbl 1275.68086 [65] Mosses, P.D., Modular structural operational semantics, Journal of logic and algebraic programming, 60-61, 195-228, (2004) · Zbl 1072.68061 [66] G. Nadathur, D. Miller, An overview of Lambda-PROLOG, in: K.A.B. Robert, A. Kowalski (Eds.), Logic Programming, Proceedings of the Fifth International Conference and Symposium, Seattle, Washington, August 15-19, 1988, Proceedings, MIT Press, 1988, pp. 810-827. [67] P.C. Ölveczky, J. Meseguer, Real-time Maude 2.1, in: N. Martí-Oliet (Ed.), Proceedings of the Fifth International Workshop on Rewriting Logic and its Applications (WRLA 2004), Electronic Notes in Theoretical Computer Science, vol. 117, Elsevier, 2005, pp. 285-314. [68] F. Pfenning, C. Elliott, Higher-order abstract syntax, in: PLDI ’88: Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation, ACM Press, New York, NY, USA, 1988, pp. 199-208. [69] Pierce, B., Types and programming languages, (2002), MIT Press [70] G.D. Plotkin, A structural approach to operational semantics, Journal of Logic and Algebraic Programming 60-61 (2004) 17-139, Original version: University of Aarhus Technical Report DAIMI FN-19, 1981. [71] Reynolds, J.C., The discoveries of continuations, Lisp and symbolic computation, 6, 3-4, 233-248, (1993) [72] G. Roşu, K: a Rewrite-based Framework for Modular Language Design, Semantics, Analysis and Implementation, Technical Report UIUCDCS-R-2005-2672, Department of Computer Science, University of Illinois at Urbana-Champaign, 2005, K was first introduced in 2003, in the technical report UIUCDCS-R-2003-2897: lecture notes of CS322 (programming language design). [73] G. Rosu, R.P. Venkatesan, J. Whittle, L. Leustean, Certifying optimality of state estimation programs, in: W.A. Hunt Jr., F. Somenzi (Eds.), Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings, Lecture Notes in Computer Science, vol. 2725, Springer, 2003, pp. 301-314. · Zbl 1278.68193 [74] Sabry, A.; Felleisen, M., Reasoning about programs in continuation-passing style, Lisp and symbolic computation, 6, 3-4, 289-360, (1993) [75] R. Sasse, Taclets vs. Rewriting Logic—Relating Semantics of Java, Master’s thesis, Fakultät für Informatik, Universität Karlsruhe, Germany, May 2005, Technical Report in Computing Science No. 2005-16. [76] R. Sasse, J. Meseguer, Java+ITP: a verification tool based on hoare logic and algebraic semantics, in: G. Denker, C. Talcott (Eds.), Proceedings of the Sixth International Workshop on Rewriting Logic and its Applications (WRLA 2006), Electronic Notes in Theoretical Computer Science, vol. 176, No. 4, Elsevier, 2007, pp. 29-46. [77] Schmidt, D.A., Denotational semantics—A methodology for language development, (1986), Allyn and Bacon Boston, MA [78] D. Scott, Outline of a mathematical theory of computation, in: Proceedings, Fourth Annual Princeton Conference on Information Sciences and Systems, Princeton University, 1970, pp. 169-176, Also appeared as Technical Monograph PRG 2, Oxford University, Programming Research Group. [79] D. Scott, C. Strachey, Toward a mathematical semantics for computer languages, in: Microwave Research Institute Symposia Series, Proceedings of the Symposium on Computers and Automata, vol. 21, Polytechnical Institute of Brooklyn, 1971. · Zbl 0268.68004 [80] Slonneger, K.; Kurtz, B.L., Formal syntax and semantics of programming languages, (1995), Addison-Wesley · Zbl 0844.68016 [81] Stärk, R.F.; Schmid, J.; Börger, E., Java and the Java virtual machine: definition, verification, validation, (2001), Springer · Zbl 0978.68033 [82] M.-O. Stehr, CINNI—a generic calculus of explicit substitutions and its application to lambda-, sigma- and pi- calculi, in: K. Futatsugi (Ed.), Proceedings of the Third International Workshop on Rewriting Logic and its Applications (WRLA 2000), Electronic Notes in Theoretical Computer Science, vol. 36, Elsevier, 2000. · Zbl 0966.68147 [83] M.-O. Stehr, I. Cervesato, S. Reich, An execution environment for the MSR cryptoprotocol specification language, 2004. Available from: . [84] M.-O. Stehr, C.L. Talcott, Plan in Maude: specifying an active network programming language, in: F. Gadducci, U. Montanari (Eds.), Proceedings of the Forth International Workshop on Rewriting Logic and its Applications (WRLA 2002), Electronic Notes in Theoretical Computer Science, vol. 71, Elsevier, 2002, pp. 240-260. · Zbl 1272.68044 [85] M.-O. Stehr, C.L. Talcott, Practical techniques for language design and prototyping, in: J.L. Fiadeiro, U. Montanari, M. Wirsing (Eds.), Abstracts Collection of the Dagstuhl Seminar 05081 on Foundations of Global Computing, February 20-25, 2005, Schloss Dagstuhl, Wadern, Germany, 2005. [86] P. Thati, K. Sen, N. Martí-Oliet, An executable specification of asynchronous Pi-Calculus semantics and may testing in Maude 2.0, in: F. Gadducci, U. Montanari (Eds.), Proceedings of the Forth International Workshop on Rewriting Logic and its Applications (WRLA 2002), Electronic Notes in Theoretical Computer Science, vol. 71, Elsevier, 2002. [87] van den Brand, M.; Heering, J.; Klint, P.; Olivier, P.A., Compiling language definitions: the asf+sdf compiler, ACM transactions on programming languages and systems (TOPLAS), 24, 4, 334-368, (2002) [88] van Deursen, A.; Heering, J.; Klint, P., Language prototyping: an algebraic specification approach, (1996), World Scientific · Zbl 0962.68114 [89] A. Verdejo, Maude como marco semántico ejecutable, Ph.D. thesis, Facultad de Informática, Universidad Complutense, Madrid, Spain, 2003. [90] A. Verdejo, N. Martí-Oliet, Implementing CCS in Maude 2, in: F. Gadducci, U. Montanari (Eds.), Proceedings of the Forth International Workshop on Rewriting Logic and its Applications (WRLA 2002), Electronic Notes in Theoretical Computer Science, vol. 71, Elsevier, 2002. [91] Verdejo, A.; Martí-Oliet, N., Executable structural operational semantics in maude, Journal of logic and algebraic programming, 67, 1-2, 226-293, (2006) · Zbl 1088.68095 [92] Viry, P., Equational rules for rewriting logic, Theoretical computer science, 285, 2, 487-517, (2002) · Zbl 1001.68058 [93] E. Visser, Program transformation with Stratego/XT: rules, strategies, tools, and systems in Stratego/XT 0.9, in: C. Lengauer, D.S. Batory, C. Consel, M. Odersky (Eds.), Domain-Specific Program Generation, International Seminar, Dagstuhl Castle, Germany, March 23-28, 2003, Revised Papers, Lecture Notes in Computer Science, vol. 3016, Springer, 2003, pp. 216-238. [94] P. Wadler, The essence of functional programming, in: POPL ’92: Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM Press, New York, NY, USA, 1992, pp. 1-14. [95] Wand, M., First-order identities as a defining language, Acta informatica, 14, 337-357, (1980) · Zbl 0424.68022 [96] Wright, A.K.; Felleisen, M., A syntactic approach to type soundness, Information and computation, 115, 1, 38-94, (1994) · Zbl 0938.68559 [97] Y. Xiao, Z.M. Ariola, M. Mauny, From syntactic theories to interpreters: a specification language and its compilation, The Computing Research Repository (CoRR), cs.PL/0009030, September 2000.
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.