CafeOBJ
From MaRDI portal
Cited in
(only showing first 100 items - show all)- A semantic approach to interpolation
- HasCasl: integrated higher-order specification and program development
- A rewriting logic approach to operational semantics
- Operational termination of conditional term rewriting systems
- Vivid: a framework for heterogeneous problem solving
- Extra theory morphisms for institutions: Logical semantics for multi-paradigm languages
- HasCasl
- Stratego
- Vivid
- CoFI
- MobileOBJ
- JavaFAN
- LARCH
- ELAN
- CASL
- SPINS
- ITP/OCL
- Swinging types=functions+relations+transition systems
- A hidden agenda
- CCSL
- TRAM
- 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
- Rewriting logic: Roadmap and bibliography
- The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors
- Automatic synthesis of logical models for order-sorted first-order theories
- A formal proof generator from semi-formal proof documents
- On combining algebraic specifications with first-order logic via Athena
- OBJ3
- CIRC
- Maude
- Relating CASL with other specification languages: the institution level.
- Relaxed models for rewriting logic
- A hidden Herbrand theorem: Combining the object and logic paradigms
- Structured theories and institutions
- Interpolation in Grothendieck institutions
- Kumo
- 2OBJ
- Hets
- Principles of proof scores in CafeOBJ
- Twenty years of rewriting logic
- Observational interpretations of hybrid dynamic logic with binders and silent transitions
- AProVE
- MMT
- CiMPG+F: a proof generator and fixer-upper for CafeOBJ specifications
- PMaude
- PVeStA
- VESTA
- PAGODA
- K tool
- K-Maude
- MFE
- CSI
- CRC 3
- MTT
- ITP
- SCC
- Birkhoff completeness for hybrid-dynamic first-order logic
- Introducing H, an institution-based formal specification and verification language
- UML2Alloy
- DDebugger
- GROVER
- CafePie
- MU-TERM
- MOMENT2
- Dist-Orc
- CARIBOO
- VMTL
- Jambox
- Saigawa
- TPA
- Tsukuba
- Marvin
- InvA
- BMaude
- Stability of termination and sufficient-completeness under pushouts via amalgamation
- Forcing, downward Löwenheim-Skolem and omitting types theorems, institutionally
- Proving operational termination of membership equational programs
- Ground confluence of order-sorted conditional specifications modulo axioms
- Formalizing provable anonymity in Isabelle/HOL
- Foundations of logic programming in hybrid logics with user-defined sharing
- Constructor-based observational logic
- Ultraproducts and possible worlds semantics in institutions
- Maude-NPA
- A modular order-sorted equational generalization algorithm
- Comorphisms of structured institutions
- Domain science and engineering from computer science to the sciences of informatics. I: Engineering
- Soundness in verification of algebraic specifications with OBJ
- Institution-independent model theory
- CoCasl
- Semantic foundations for generalized rewrite theories
- Conditional Confluence
- UNITY
- Behavioural specification for hierarchical object composition
- Equational formulas and pattern operations in initial order-sorted algebras
- Behavioral and coinductive rewriting
- Parameterized theories and views in full Maude 2. 0
This page was built for software: CafeOBJ