OBJ3

swMATH5370MaRDI QIDQ17510

No author found.

Related Items (only showing first 100 items - show all)

Gordon's computer: A hardware verification case study in OBJ3 ⋮ Structured theories and institutions ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Invariant-driven specifications in Maude ⋮ Equational formulas and pattern operations in initial order-sorted algebras ⋮ Unnamed Item ⋮ The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors ⋮ Quasi-Boolean encodings and conditionals in algebraic specification ⋮ Verifying a distributed list system: A case history ⋮ Translating a Dependently-Typed Logic to First-Order Logic ⋮ Order-Sorted Parameterization and Induction ⋮ Creol: A type-safe object-oriented model for distributed concurrent systems ⋮ Category-based modularisation for equational logic programming ⋮ Modular and incremental proofs of AC-termination ⋮ Proving termination of context-sensitive rewriting by transformation ⋮ 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 ⋮ Unnamed Item ⋮ Morphism axioms ⋮ Mechanising the theory of intervals using OBJ3 ⋮ Essential concepts of algebraic specification and program development ⋮ Program tactics and logic tactics ⋮ Parameterisation for abstract structured specifications ⋮ Two Decades of Maude ⋮ Function Calls at Frozen Positions in Termination of Context-Sensitive Rewriting ⋮ A scalable module system ⋮ Principles of proof scores in CafeOBJ ⋮ Order-sorted algebraic specifications with higher-order functions ⋮ May I borrow your logic? (Transporting logical structures along maps) ⋮ Abstract data type systems ⋮ Twenty years of rewriting logic ⋮ An axiomatic approach to structuring specifications ⋮ A modular order-sorted equational generalization algorithm ⋮ Computationally Equivalent Elimination of Conditions ⋮ Unnamed Item ⋮ Algorithm theories and design tactics ⋮ A metamodel of access control for distributed environments: applications and properties ⋮ An Algebraic Approach to Compiler Design ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Termination of Rewriting with Strategy Annotations ⋮ A survey of strategies in rule-based program transformation systems ⋮ Specification and proof in membership equational logic ⋮ Partial derivatives of regular expressions and finite automaton constructions ⋮ Conditional rewriting logic as a unified model of concurrency ⋮ Institution-independent model theory ⋮ Strict coherence of conditional rewriting modulo axioms ⋮ The formal specification of safety requirements for storing explosives ⋮ A Maude environment for CafeOBJ ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Institution morphisms ⋮ On the algebra of structured specifications ⋮ Behavioral abstraction is hiding information ⋮ Proving operational termination of membership equational programs ⋮ An overview of the K semantic framework ⋮ Algebraic correctness proofs for compiling recursive function definitions with strictness information ⋮ Context-sensitive dependency pairs ⋮ An Object-Oriented Component Model for Heterogeneous Nets ⋮ An encoding of partial algebras as total algebras ⋮ Normal forms and normal theories in conditional rewriting ⋮ First-Order Logic with Dependent Types ⋮ A Modular Equational Generalization Algorithm ⋮ Programming and symbolic computation in Maude ⋮ Ground confluence of order-sorted conditional specifications modulo axioms ⋮ Applications and extensions of context-sensitive rewriting ⋮ Using Context-Sensitive Rewriting for Proving Innermost Termination of Rewriting ⋮ Methods for Proving Termination of Rewriting-based Programming Languages by Transformation ⋮ A rewriting logic approach to operational semantics ⋮ Algebraic models of microprocessors architecture and organisation ⋮ Derivational complexity and context-sensitive Rewriting ⋮ Unnamed Item ⋮ Just-in-time ⋮ Interpreting Abstract Interpretations in Membership Equational Logic ⋮ Lazy Rewriting and Context-Sensitive Rewriting ⋮ A hidden agenda ⋮ Towards Behavioral Maude ⋮ Operational termination of conditional term rewriting systems ⋮ On-demand strategy annotations revisited: an improved on-demand evaluation strategy ⋮ Behavioural specification for hierarchical object composition ⋮ CASL: the Common Algebraic Specification Language. ⋮ Relating CASL with other specification languages: the institution level. ⋮ Context-sensitive rewriting strategies ⋮ A hidden Herbrand theorem: Combining the object and logic paradigms ⋮ Formal specification of topological subdivisions using hypermaps ⋮ Using CafeOBJ to Mechanise Refactoring Proofs and Application ⋮ The role of logical interpretations in program development ⋮ A Rewriting Logic Approach to Operational Semantics (Extended Abstract) ⋮ Maude: specification and programming in rewriting logic ⋮ Logical foundations of CafeOBJ ⋮ Equational rules for rewriting logic ⋮ Constructing specification morphisms ⋮ Normal form approach to compiler design ⋮ OBSCURE, a specification language for abstract data types ⋮ FORMAL VALIDATION AND VERIFICATION OF ATOMIC RESOLUTION MICROSCOPE CONTROL AND TOPOGRAPHY

This page was built for software: OBJ3