scientific article

Răzvan Diaconescu, Kokichi Futatsugi

Publication date: 29 May 2001

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

CafeOBJ algebraic specification language

Theory of programming languages (68N15) Abstract data types; algebraic specification (68Q65) Research exposition (monographs, survey articles) pertaining to computer science (68-02)

Related Items

Foundations of logic programming in hybrid logics with user-defined sharing, Rewriting logic: Roadmap and bibliography, Bisimulation and Hidden Algebra, Constructor-based observational logic, Structured theories and institutions, Interpolation in Grothendieck institutions, Equational formulas and pattern operations in initial order-sorted algebras, Ultraproducts and possible worlds semantics in institutions, Behavioral equivalence of hidden \(k\)-logics: an abstract algebraic approach, The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors, A Proof Score Approach to Formal Verification of an Imperative Programming Language Compiler, Algebraic simulations, Quasi-Boolean encodings and conditionals in algebraic specification, Order-Sorted Parameterization and Induction, Automatic synthesis of logical models for order-sorted first-order theories, Functorial semantics of first-order views, Dependency pairs for proving termination properties of conditional term rewriting systems, Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic, Parameterisation for abstract structured specifications, Principles of proof scores in CafeOBJ, Introducing \(H\), an institution-based formal specification and verification language, A short overview of Hidden Logic, Twenty years of rewriting logic, Foundations for structuring behavioural specifications, Variants and satisfiability in the infinitary unification wonderland, Partialising institutions, An axiomatic approach to structuring specifications, A modular order-sorted equational generalization algorithm, Stability of termination and sufficient-completeness under pushouts via amalgamation, Comorphisms of structured institutions, MTT: The Maude Termination Tool (System Description), Observational interpretations of hybrid dynamic logic with binders and silent transitions, Equational abstractions, CafeOBJ Traces, Parchments for CafeOBJ Logics, Towards a Combination of CafeOBJ and PAT, Behavioral Rewrite Systems and Behavioral Productivity, An Institution for Imperative RSL Specifications, Verifying the Design of Dynamic Software Updating in the OTS/CafeOBJ Method, On Automation of OTS/CafeOBJ Method, Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs, Soundness in verification of algebraic specifications with OBJ, Strict coherence of conditional rewriting modulo axioms, A Maude environment for CafeOBJ, Forcing, downward Löwenheim-Skolem and omitting types theorems, institutionally, A Transformational Approach to Prove Outermost Termination Automatically, Unnamed Item, On the algebra of structured specifications, Behavioral abstraction is hiding information, Equational Formulas and Pattern Operations in Initial Order-Sorted Algebras, Operational Termination of Membership Equational Programs: the Order-Sorted Way, Proving operational termination of membership equational programs, Structural induction in institutions, Semantic foundations for generalized rewrite theories, An encoding of partial algebras as total algebras, Saturated models in institutions, Normal forms and normal theories in conditional rewriting, Integrating Maude into Hets, A Modular Equational Generalization Algorithm, Ground confluence of order-sorted conditional specifications modulo axioms, A semantic approach to interpolation, HasCasl: integrated higher-order specification and program development, Methods for Proving Termination of Rewriting-based Programming Languages by Transformation, Order-Sorted Rewriting and Congruence Closure, A rewriting logic approach to operational semantics, Order-Sorted Generalization, Swinging types=functions+relations+transition systems, A hidden agenda, Towards Behavioral Maude, Operational termination of conditional term rewriting systems, Behavioural specification for hierarchical object composition, Relating CASL with other specification languages: the institution level., Relaxed models for rewriting logic, A hidden Herbrand theorem: Combining the object and logic paradigms, A Rewriting Logic Approach to Operational Semantics (Extended Abstract), Dynamic connectors for concurrency, Maude: specification and programming in rewriting logic, Logical foundations of CafeOBJ, Comparing logics for rewriting: Rewriting logic, action calculi and tile logic, Specification of real-time and hybrid systems in rewriting logic

Uses Software

CafeOBJ