Towards behavioral maude: Behavioral membership equational logic

Research output: Contribution to journalConference articlepeer-review


How can algebraic and coalgebraic specifications be integrated? How can behavioral equivalence be addressed in an algebraic specification language? The hidden-sorted approach, originating in work of Goguen and Meseguer in the early 80's, and further developed into the hidden-sorted logic approach by researchers at Oxford, UC San Diego, and Kanazawa offers some attractive answers, and has been implemented in both BOBJ and CafeOBJ. In this work we investigate both further extensions of hidden logic, and an extension of the Maude specification language called BMaude supporting this extended hidden-sorted semantics. Maude's underlying equational logic, membership equational logic, generalizes and increases the expressive power of many-sorted and order-sorted equational logics. We develop a hidden-sorted extension of membership equational logic, and give conditions under which theories have both an algebraic and a coalgebraic semantics, including final (co-)algebras. We also discuss the language design of BMaude, based on such an extended logic and using categorical notions in and across the different institutions involved. We also explain how Maude's reflective semantics provides a systematic method to extend Maude to BMaude within Maude, including module composition operations, evaluation, and automated proof methods.

Original languageEnglish (US)
Pages (from-to)197-253
Number of pages57
JournalElectronic Notes in Theoretical Computer Science
Issue number1
StatePublished - Oct 2002
EventCMCS'2002, Coalgebraic Methods in Computer Science (Satellite Event of ETAPS 2002) - Grenoble, France
Duration: Apr 6 2002Apr 7 2002


  • Coalgebra
  • Maude
  • Membership and hidden algebra

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Towards behavioral maude: Behavioral membership equational logic'. Together they form a unique fingerprint.

Cite this