Abstract
The OBJ algebraic specification language and its Eqlog and FOOPS multiparadigm extensions are revisited from the perspective of the Maude language design. A common thread is the quest for ever more expressive computational logics, on which executable formal specifications of increasingly broader classes of systems can be based. Several recent extensions, beyond Maude itself, are also discussed.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
- Module Algebra
- Computational Logic
- Equational Logic
- Statistical Model Check
- Structural Operational Semantic
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Agha, G.: Actors. MIT Press, Cambridge (1986)
Agha, G., Gunter, C., Greenwald, M., Khanna, S., Meseguer, J., Sen, K., Thati, P.: Formal modeling and analysis of DoS using probabilistic rewrite theories. In: Proc. Workshop on Foundations of Computer Security (FCS 2005) (Affiliated with LICS 2005) (2005)
Agha, G., Hewitt, C.: Concurrent programming using actors. In: Yonezawa, A., Tokoro, M. (eds.) Object-Oriented Concurrent Programming, pp. 37–53. MIT Press, Cambridge (1988)
Agha, G., Meseguer, J., Sen, K.: PMaude: Rewrite-based specification language for probabilistic object systems. In: 3rd Workshop on Quantitative Aspects of Programming Languages, QAPL 2005 (2005)
Basin, D., Clavel, M., Meseguer, J.: Rewriting logic as a metalogical framework. In: Kapoor, S., Prasad, S. (eds.) FST TCS 2000. LNCS, vol. 1974, pp. 55–80. Springer, Heidelberg (2000)
Basin, D., Clavel, M., Meseguer, J.: Rewriting logic as a metalogical framework. ACM Transactions on Computational Logic 5, 528–576 (2004)
Basin, D., Denker, G.: Maude versus Haskell: an experimental comparison in security protocol analysis. In: Futatsugi, K. (ed.) Proc. 3rd. Intl. Workshop on Rewriting Logic and its Applications. ENTCS, vol. 36, Elsevier, Amsterdam (2000)
Berardi, S.: Towards a mathematical analysis of the Coquand-Huet calculus of constructions and other systems in barendregt’s cube. Technical Report, Carnegie- Mellon University and Università di Torino (1988)
Bernot, G., Bidoit, M., Knapik, T.: Observational specifications and the indistinguishability assumption. Theoretical Comp. Science 139(1-2), 275–314 (1995)
Berregeb, N., Bouhoula, A., Rusinowitch, M.: Observational proofs with critical contexts. In: Astesiano, E. (ed.) ETAPS 1998 and FASE 1998. LNCS, vol. 1382, p. 38. Springer, Heidelberg (1998)
Bidoit, M., Hennicker, R.: Observer complete definitions are behaviourally coherent. In: OBJ/CafeOBJ/Maude at Formal Methods 1999, Theta, pp. 83–94 (1999)
Bouhoula, A., Jouannaud, J.-P., Meseguer, J.: Specification and proof in membership equational logic. Theoretical Computer Science 236, 35–132 (2000)
Bruni, R., Meseguer, J.: Generalized rewrite theories. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 252–266. Springer, Heidelberg (2003)
Burstall, R., Goguen, J.A.: The semantics of Clear, a specification language. In: Bjorner, D. (ed.) Abstract Software Specifications. LNCS, vol. 86, pp. 292–332. Springer, Heidelberg (1980)
Clavel, M.: Reflection in general logics and in rewriting logic, with applications to the Maude language. Ph.D. Thesis, University of Navarre (1998)
Clavel, M.: Reflection in Rewriting Logic: Metalogical Foundations and Metaprogramming Applications. CSLI Publications, Stanford (2000)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J.: Metalevel computation in Maude. In: Proc. 2nd Intl. Workshop on Rewriting Logic and its Applications. ENTCS, vol. 15, North-Holland, Amsterdam (1998)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.: Maude: specification and programming in rewriting logic. Theoretical Computer Science 285, 187–243 (2002)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: Maude Manual (Version 2.2) (December 2005), http://maude.cs.uiuc.edu
Clavel, M., Durán, F., Eker, S., Meseguer, J.: Building equational proving tools by reflection in rewriting logic. In: CAFE: An Industrial-Strength Algebraic Formal Method, Elsevier, Amsterdam (2000), http://maude.cs.uiuc.edu
Clavel, M., Durán, F., Eker, S., Meseguer, J., Stehr, M.-O.: Maude as a formal meta-tool. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol. 1709, pp. 1684–1703. Springer, Heidelberg (1999)
Clavel, M., Durán, F., Martí-Oliet, N.: Polytypic programming in Maude. In: Proc. 3rd. Intl. Workshop on Rewriting Logic and its Applications. ENTCS, vol. 36, Elsevier, Amsterdam (2000)
Clavel, M., Meseguer, J.: Axiomatizing reflective logics and languages. In: Kiczales, G. (ed.) Proceedings of Reflection 1996, San Francisco, California, April 1996, pp. 263–288 (1996), http://jerry.cs.uiuc.edu/reflection/
Clavel, M., Meseguer, J.: Reflection and strategies in rewriting logic. In: Meseguer, J. (ed.) Proc. First Intl. Workshop on Rewriting Logic and its Applications. Electronic Notes in Theoretical Computer Science, vol. 4, Elsevier, Amsterdam (1996)
Clavel, M., Meseguer, J.: Reflection in conditional rewriting logic. Theoretical Computer Science 285, 245–288 (2002)
Clavel, M., Meseguer, J., Palomino, M.: Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic. In: Gadducci, F., Montanari, U. (eds.) 4th. Intl. Workshop on Rewriting Logic and its Applications. ENTCS, Elsevier, Amsterdam (2002)
Clavel, M., Palomino, M.: The ITP tool’s manual. Universidad Complutense, Madrid (April 2005), http://maude.sip.ucm.es/itp/
Coquand, T., Huet, G.: The calculus of constructions. Information and Computation 76, 95–120 (1988)
Diaconescu, R.: Hidden sorted rewriting logic. In: Meseguer, J. (ed.) Proc. First Intl. Workshop on Rewriting Logic and its Applications, 4th edn. Electronic Notes in Theoretical Computer Science, Elsevier, Amsterdam (1996)
Diaconescu, R., Futatsugi, K.: Behavioral coherence in object-oriented algebraic specification. Journal of Universal Computer Science 6(1), 74–96 (2000)
Diaconescu, R., Futatsugi, K.: Logical foundations of CafeOBJ. Theoretical Computer Science 285, 289–318 (2001)
Durán, F.: A reflective module algebra with applications to the Maude language. Ph.D. Thesis, University of Málaga (1999)
Durán, F.: Coherence checker and completion tools for Maude specifications. Computer Science Laboratory, SRI International (2000) (manuscript), http://maude.cs.uiuc.edu/papers
Durán, F.: Termination checker and Knuth-Bendix completion tools for Maude equational specifications. Computer Science Laboratory, SRI International (2000) (manuscript), http://maude.cs.uiuc.edu/papers
Durán, F., Eker, S., Lincoln, P., Meseguer, J.: Principles of Mobile Maude. In: Kotz, D., Mattern, F. (eds.) MA 2000, ASA/MA 2000, and ASA 2000. LNCS, vol. 1882, pp. 73–85. Springer, Heidelberg (2000)
Durán, F., Lucas, S., Meseguer, J., Marché, C., Urbain, X.: Proving termination of membership equational programs. In: Sestoft, P., Heintze, N. (eds.) Proc. of ACM SIGPLAN 2004 Symposium on Partial Evaluation and Program Manipulation, PEPM 2004, pp. 147–158. ACM Press, New York (2004)
Durán, F., Meseguer, J.: An extensible module algebra for Maude. In: Proc. 2nd Intl. Workshop on Rewriting Logic and its Applications. ENTCS, vol. 15, North-Holland, Amsterdam (1998)
Durán, F., Meseguer, J.: A Church-Rosser checker tool for Maude equational specifications. Computer Science Laboratory, SRI International (2000) (manuscript), http://maude.cs.uiuc.edu/papers
Durán, F., Meseguer, J.: On parameterized theories and views in Full Maude 2.0. In: Futatsugi, K. (ed.) Proc. 3rd. Intl. Workshop on Rewriting Logic and its Applications. ENTCS, vol. 36, Elsevier, Amsterdam (2000)
Eker, S.: Term rewriting with operator evaluation strategy. In: Proc. 2nd Intl. Workshop on Rewriting Logic and its Applications. ENTCS, vol. 15, North-Holland, Amsterdam (1998)
Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL model checker. In: Gadducci, F., Montanari, U. (eds.) Proc. 4th. Intl. Workshop on Rewriting Logic and its Applications. ENTCS, Elsevier, Amsterdam (2002)
Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL model checker and its implementation. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 230–234. Springer, Heidelberg (2003)
Escobar, S., Meadows, C., Meseguer, J.: A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties (2005) (submitted for publication)
Escobar, S., Meadows, C., Meseguer, J.: A rewriting-based inference system for the NRL protocol analyzer: Grammar generation. In: Proc. FMSE 2005, Formal Methods in Security Engineering, Alexandria, Virginia, November 2005, pp. 1–12. ACM Press, New York (2005)
Escobar, S., Meseguer, J., Thati, P.: Natural narrowing for general term rewriting systems. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 279–293. Springer, Heidelberg (2005)
Futatsugi, K., Diaconescu, R.: CafeOBJ Report. AMAST Series. World Scientific, Singapore (1998)
Futatsugi, K., Goguen, J., Jouannaud, J.-P., Meseguer, J.: Principles of OBJ2. In: Reid, B. (ed.) Proceedings of 12th ACM Symposium on Principles of Programming Languages, pp. 52–66. ACM Press, New York (1985)
Glynn, P.: The role of generalized semi-Markov processes in simulation output analysis (1983)
Goguen, J.: Order sorted algebra. Technical Report Semantics and Theory of Computation Report 14, UCLA (1978)
Goguen, J.: Types as theories. In: Topology and Category Theory in Computer Science, Oxford, pp. 357–390 (1991)
Goguen, J., Diaconescu, R.: Towards an algebraic semantics for the object paradigm. In: Ehrig, H., Orejas, F. (eds.) Abstract Data Types 1992 and COMPASS 1992. LNCS, vol. 785, Springer, Heidelberg (1994)
Goguen, J., Jouannaud, J.-P., Meseguer, J.: Operational semantics of ordersorted algebra. In: Brauer, W. (ed.) ICALP 1985. LNCS, vol. 194, pp. 221–231. Springer, Heidelberg (1985)
Goguen, J., Kirchner, C., Kirchner, H., Mégrelis, A., Meseguer, J., Winkler, T.: An introduction to OBJ3. In: Kaplan, S., Jouannaud, J.-P. (eds.) CTRS 1987. LNCS, vol. 308, pp. 258–263. Springer, Heidelberg (1988)
J. Goguen, K. Lin, and G. Roşu. Circular coinductive rewriting. In Proceedings, 15th International Conference on Automated Software Engineering (ASE 2000). Institute of Electrical and Electronics Engineers Computer Society, Grenoble, France (September 11-15, 2000)
Goguen, J., Malcolm, G.: Hidden coinduction: Behavioral correctness proofs for objects. Mathematical Structures in Computer Science 9(3), 287–319 (1999)
Goguen, J., Malcolm, G.: A hidden agenda. J. of TCS 245(1), 55–101 (2000)
Goguen, J., Meseguer, J.: Correctness of recursive flow diagram programs. In: Gruska, J. (ed.) MFCS 1977. LNCS, vol. 53, pp. 580–595. Springer, Heidelberg (1977)
Goguen, J., Meseguer, J.: Universal realization, persistent interconnection and implementation of abstract modules. In: Nielsen, M., Schmidt, E.M. (eds.) ICALP 1982. LNCS, vol. 140, pp. 265–281. Springer, Heidelberg (1982)
Goguen, J., Meseguer, J.: Equality, types, modules and (why not?) generics for logic programming. Journal of Logic Programming 1(2), 179–210 (1984)
Goguen, J., Meseguer, J.: Models and equality for logical programming. In: Ehrig, H., Levi, G., Montanari, U. (eds.) TAPSOFT 1987 and CFLP 1987. LNCS, vol. 250, pp. 1–22. Springer, Heidelberg (1987)
Goguen, J., Meseguer, J.: Unifying functional, object-oriented and relational programming with logical semantics. In: Shriver, B., Wegner, P. (eds.) Research Directions in Object-Oriented Programming, pp. 417–477. MIT Press, Cambridge (1987)
Goguen, J., Meseguer, J.: Order-sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoretical Computer Science 105, 217–273 (1992)
Goguen, J., Meseguer, J., Plaisted, D.: Programming with parameterized abstract objects in OBJ. In: Ferrari, D., Bolognani, M., Goguen, J. (eds.) Theory and Practice of Software Technology, pp. 163–193. North-Holland, Amsterdam (1983)
Goguen, J., Roşu, G.: Hiding more of hidden algebra. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol. 1709, pp. 1704–1719. Springer, Heidelberg (1999)
Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.-P.: Introducing OBJ. In: Software Engineering with OBJ: Algebraic Specification in Action, pp. 3–167. Kluwer, Dordrecht (2000)
Goguen, J.A., Malcolm, G.: Software Engineering with OBJ: Algebraic Specification in Action. In: Advances in Formal Methods, vol. 2, Kluwer Academic Publishers, Boston (2000) ISBN 0-7923-7757-5
Hendrix, J., Clavel, M., Meseguer, J.: A sufficient completeness reasoning tool for partial specifications. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 165–174. Springer, Heidelberg (2005)
Hennicker, R., Bidoit, M.: Observational logic. In: Haeberer, A.M. (ed.) AMAST 1998. LNCS, vol. 1548, pp. 263–277. Springer, Heidelberg (1998)
Holzmann, G.: The Spin Model Checker - Primer and Reference Manual. Addison- Wesley, Reading (2003)
Kirchner, C., Kirchner, H., Meseguer, J.: Operational semantics of OBJ3. In: Lepistö, T., Salomaa, A. (eds.) ICALP 1988. LNCS, vol. 317, pp. 287–301. Springer, Heidelberg (1988)
Kosiuczenko, P., Wirsing, M.: Timed rewriting logic with application to object-oriented specification. Technical report, Institut für Informatik, Universit ät München (1995)
Kumar, N., Sen, K., Meseguer, J., Agha, G.: Probabilistic rewrite theories: Unifying models, logics and tools. Technical Report UIUCDCS-R-2003-2347, CS Dept. University of Illinois at Urbana-Champaign (May 2003)
Kumar, N., Sen, K., Meseguer, J., Agha, G.: A rewriting based model for probabilistic distributed object systems. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 32–46. Springer, Heidelberg (2003)
Lien, E.: Formal modeling and analysis of the NORM multicast protocol in Real- Time Maude. Master’s thesis, Dept. of Linguistics, University of Oslo (April 2004), http://wo.uio.no/as/WebObjects/theses.woa/wo/0.3.9
Lucas, S.: Context-sensitive computations in functional and functional logic programs. J. Functl. and Log. Progr. 1(4), 446–453 (1998)
Lucas, S.: Termination of on-demand rewriting and termination of obj programs. In: PPDP 1999, pp. 82–93. ACM, New York (2001)
Lucas, S.: Termination of rewriting with strategy annotations. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 669–684. Springer, Heidelberg (2001)
Lucas, S.: Context-sensitive rewriting strategies. Inf. Comput. 178(1), 294–343 (2002)
Lucas, S., Marché, C., Meseguer, J.: Operational termination of conditional term rewriting systems. Information Processing Letters 95(4), 446–453 (2005)
Manes, E.: Proceedings of the First International Symposium on Category Theory Applied to Computation and Control. In: Category Theory Applied to Computation and Control. LNCS, vol. 25, pp. 25–26. Springer, Heidelberg (1975)
Martí-Oliet, N., Meseguer, J.: Rewriting logic as a logical and semantic framework. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, 2nd edn., pp. 1–87. Kluwer Academic Publishers, Dordrecht (2002), First published as SRI Tech. Report SRI-CSL-93-05 (August 1993)
Martí-Oliet, N., Meseguer, J.: Rewriting logic: roadmap and bibliography. Theoretical Computer Science 285, 121–154 (2002)
Martí-Oliet, N., Meseguer, J., Verdejo, A.: Towards a strategy language for Maude. In: Martí-Oliet, N. (ed.) Proc. 5th. Intl. Workshop on Rewriting Logic and its Applications. ENTCS, pp. 417–441. Elsevier, Amsterdam (2004)
Meadows, C.: The NRL protocol analyzer: An overview. Journal of Logic Programming 26(2), 113–131 (1996)
Meseguer, J.: General logics. In: H.-D.E., et al. (eds.) Logic Colloquium 1987, pp. 275–329. North-Holland, Amsterdam (1989)
Meseguer, J.: A logical theory of concurrent objects. In: ECOOP-OOPSLA 1990 Conference on Object-Oriented Programming, Ottawa, Canada, October 1990, pp. 101–115. ACM, New York (1990)
Meseguer, J.: Rewriting as a unified model of concurrency. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 384–400. Springer, Heidelberg (1990)
Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992)
Meseguer, J.: Multiparadigm logic programming. In: Kirchner, H., Levi, G. (eds.) ALP 1992. LNCS, vol. 632, pp. 158–200. Springer, Heidelberg (1992)
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. MIT Press, Cambridge (1993)
Meseguer, J.: Solving the inheritance anomaly in concurrent object-oriented programming. In: Nierstrasz, O. (ed.) ECOOP 1993. LNCS, vol. 707, pp. 220–246. Springer, Heidelberg (1993)
Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18–61. Springer, Heidelberg (1998)
Meseguer, J.: A rewriting logic sampler. In: Van Hung, D., Wirsing, M. (eds.) ICTAC 2005. LNCS, vol. 3722, pp. 1–28. Springer, Heidelberg (2005)
Meseguer, J., Goguen, J.: Initiality, induction and computability. In: Nivat, M., Reynolds, J. (eds.) Algebraic Methods in Semantics, pp. 459–541. Cambridge University Press, Cambridge (1985)
Meseguer, J., Roşu, G.: A total approach to partial algebraic specification. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol. 2380, pp. 572–584. Springer, Heidelberg (2002)
Meseguer, J., Roşu, G.: Towards behavioral Maude: Behavioral membership equational logic. In: Proc. CMCS 2002, Elsevier, Amsterdam (2002)
Meseguer, J., Roşu, G.: Rewriting logic semantics: From language specifications to formal analysis tools. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 1–44. Springer, Heidelberg (2004)
Meseguer, J., Roşu, G.: The rewriting logic semantics project. In: Proc. SOS 2005. ENTCS, Elsevier, Amsterdam (2005)
Meseguer, J., Sharykin, R.: Specification and analysis of distributed objectbased stochastic hybrid systems. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 460–475. Springer, Heidelberg (2006)
Meseguer, J., Talcott, C.: Semantic models for distributed object reflection. In: Magnusson, B. (ed.) ECOOP 2002. LNCS, vol. 2374, pp. 1–36. Springer, Heidelberg (2002)
Moore, J., Krug, R., Liu, H., Porter, G.: Formal models of Java at the JVM level – a survey from the ACL2 perspective. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol. 2072, Springer, Heidelberg (2001)
Ölveczky, P.C.: Specification and Analysis of Real-Time and Hybrid Systems in Rewriting Logic. PhD thesis, University of Bergen, Norway (2000), http://maude.csl.sri.com/papers
Ölveczky, P.C., Caccamo, M.: Formal simulation and analysis of the CASH scheduling algorithm in Real-Time Maude. In: Baresi, L., Heckel, R. (eds.) FASE 2006. LNCS, vol. 3922, pp. 357–372. Springer, Heidelberg (2006)
Ölveczky, P.C., Keaton, M., Meseguer, J., Talcott, C., Zabele, S.: Specification and analysis of the AER/NCA active network protocol suite in Real-Time Maude. In: Hussmann, H. (ed.) FASE 2001. LNCS, vol. 2029, pp. 333–348. Springer, Heidelberg (2001)
Ölveczky, P.C., Kosiuczenko, P., Wirsing, M.: An object-oriented algebraic steam-boiler control specification. In: Abrial, J.-R., Börger, E., Langmaack, H. (eds.) Dagstuhl Seminar 1995. LNCS, vol. 1165, pp. 379–402. Springer, Heidelberg (1996)
Ölveczky, P.C., Meseguer, J.: Specifying real-time systems in rewriting logic. In: Meseguer, J. (ed.) Proc. First Intl. Workshop on Rewriting Logic and its Applications. Electronic Notes in Theoretical Computer Science, vol. 4, Elsevier, Amsterdam (1996)
Ölveczky, P.C., Meseguer, J.: Real-Time Maude: a tool for simulating and analyzing real-time and hybrid systems. In: Proc. 3rd. Intl. Workshop on Rewriting Logic and its Applications. ENTCS, vol. 36, Elsevier, Amsterdam (2000)
Ölveczky, P.C., Meseguer, J.: Specification of real-time and hybrid systems in rewriting logic. Theoretical Computer Science 285, 359–405 (2002)
Ölveczky, P.C., Meseguer, J.: Real-Time Maude 2.1. In: Martí-Oliet, N. (ed.) Proc. 5th. Intl. Workshop on Rewriting Logic and its Applications. ENTCS, pp. 285–314. Elsevier, Amsterdam (2004)
Ölveczky, P.C., Meseguer, J.: Specification and analysis of real-time systems using Real-Time Maude. In: Wermelinger, M., Margaria-Steffen, T. (eds.) FASE 2004. LNCS, vol. 2984, pp. 354–358. Springer, Heidelberg (2004)
Ölveczky, P.C., Meseguer, J.: Abstraction and completeness for Real-Time Maude. In: Denker, G., Talcott, C. (eds.) Proc. 6th. Intl. Workshop on Rewriting Logic and its Applications ENTCS, Elsevier, Amsterdam (2006)
Ölveczky, P.C., Meseguer, J.: Semantics and pragmatics of Real-Time Maude. Higher-Order and Symbolic Computation (2006) (to appear)
Ölveczky, P.C., Meseguer, J., Talcott, C.L.: Specification and analysis of the AER/NCA active network protocol suite in Real-Time Maude. Technical Report UIUCDCS-R-2004-2467, Department of Computer Science, University of Illinois at Urbana-Champaign (2004), Available at http://www.ifi.uio.no/RealTimeMaude
Ölveczky, P.C., Thorvaldsen, S.: Formal modeling and analysis of wireless sensor network algorithms in Real-Time Maude. In: The 14th International Workshop on Parallel and Distributed Real-Time Systems (WPDRTS) 2006, IEEE Computer Society Press, Los Alamitos (2006)
Padawitz, P.: Swinging data types: Syntax, semantics, and theory. In: Haveraaen, M., Dahl, O.-J., Owe, O. (eds.) Abstract Data Types 1995 and COMPASS 1995. LNCS, vol. 1130, pp. 409–435. Springer, Heidelberg (1996)
Padawitz, P.: Towards the one-tiered design of data types and transition systems. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 365–380. Springer, Heidelberg (1998)
Padawitz, P.: Swinging types = functions + relations + transition systems. Theoretical Computer Science 243, 93–165 (2000)
Palomino, M.: A predicate abstraction tool for Maude. Universidad Complutense (2005) (manuscript), http://maude.sip.ucm.es/miguelpt/papers/pa-tool.pdf
Puterman, M.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley and Sons, Chichester (1994)
Roşu, G.: Hidden Logic. PhD thesis, University of California at San Diego (2000)
Roşu, G., Eker, S., Lincoln, P., Meseguer, J.: Certifying and synthesizing membership equational proofs. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 359–380. Springer, Heidelberg (2003)
Roşu, G., Goguen, J.: Hidden congruent deduction. In: Caferra, R., Salzer, G. (eds.) FTP 1998. LNCS (LNAI), vol. 1761, pp. 251–266. Springer, Heidelberg (2000)
Segala, R.: Modelling and Verification of Randomized Distributed Real Time Systems. PhD thesis, Massachusetts Institute of Technology (1995)
Sen, K., Viswanathan, M., Agha, G.: On statistical model checking of stochastic systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 266–280. Springer, Heidelberg (2005)
Steggles, L., Kosiuczenko, P.: A timed rewriting logic semantics for SDL: a case study of the alternating bit protocol. In: Proc. 2nd Intl. Workshop on Rewriting Logic and its Applications. ENTCS, vol. 15, North Holland, Amsterdam (1998)
Stehr, M.-O.: CINNI - a generic calculus of explicit substitutions and its application to lambda-, sigma- and pi-calculi. In: Proc. 3rd. Intl. Workshop on Rewriting Logic and its Applications. ENTCS, Elsevier, Amsterdam (2000)
Stehr, M.-O.: Programming, Specification, and Interactive Theorem Proving — Towards a Unified Language based on Equational Logic, Rewriting Logic, and Type Theory. Doctoral Thesis, Universität Hamburg, Fachbereich Informatik, Germany (2002), http://www.sub.uni-hamburg.de/disse/810/
Stehr, M.-O.: The Open Calculus of Constructions: An equational type theory with dependent types for programming, specification, and interactive theorem proving (Part I). Fundamenta Informaticae 68(1-2), 131–174 (2005)
Stehr, M.-O.: The Open Calculus of Constructions: An equational type theory with dependent types for programming, specification, and interactive theorem proving (Part II). Fundamenta Informaticae 68(3), 249–288 (2005)
Stehr, M.-O., Meseguer, J.: Pure type systems in rewriting logic: Specifying typed higher-order languages in a first-order logical framework. In: Owe, O., Krogdahl, S., Lyche, T. (eds.) From Object-Orientation to Formal Methods. LNCS, vol. 2635, pp. 334–375. Springer, Heidelberg (2004)
Stewart, W.J.: Introduction to the Numerical Solution of Markov Chains. Princeton (1994)
Thati, P., Meseguer, J.: Symbolic reachability analysis using narrowing and its application to the verification of cryptographic protocols. In: Martí-Oliet, N. (ed.) Proc. 5th. Intl. Workshop on Rewriting Logic and its Applications. ENTCS, vol. 117, pp. 153–182. Elsevier, Amsterdam (2004)
Thati, P., Meseguer, J.: Complete symbolic reachability analysis using backand- forth narrowing. In: Fiadeiro, J.L., Harman, N.A., Roggenbach, M., Rutten, J. (eds.) CALCO 2005. LNCS, vol. 3629, pp. 379–394. Springer, Heidelberg (2005)
Thorvaldsen, S., Ölveczky, P.C.: Formal modeling and analysis of the OGDC wireless sensor network algorithm in Real-Time Maude (2005), http://www.ifi.uio.no/RealTimeMaude/OGDC
Tracz, W.: Parametrized programming in LILEANNA. In: Proc. 1993 ACM/SIGAPP Symp. on Applied Computing (SAC 1993), pp. 77–86 (1993)
Viry, P.: Equational rules for rewriting logic. Theoretical Computer Science 285, 487–517 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Meseguer, J. (2006). From OBJ to Maude and Beyond. In: Futatsugi, K., Jouannaud, JP., Meseguer, J. (eds) Algebra, Meaning, and Computation. Lecture Notes in Computer Science, vol 4060. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11780274_14
Download citation
DOI: https://doi.org/10.1007/11780274_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-35462-8
Online ISBN: 978-3-540-35464-2
eBook Packages: Computer ScienceComputer Science (R0)