A conservative look at operational semantics with variable binding

DOI10.1006/INCO.1998.2729zbMath0916.68098OpenAlexW2019447115MaRDI QIDQ1273877

Chris Verhoef, W. J. Fokkink

Publication date: 6 January 1999

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/efa7ba4abd245de7e042a344f1a692bd4b0fa5f2

zbMATH Keywords

transition system specifications

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (18)

Proving the validity of equations in GSOS languages using rule-matching bisimilarity ⋮ Modular structural operational semantics ⋮ A format for semantic equivalence comparison ⋮ A general SOS theory for the specification of probabilistic transition systems ⋮ Duplication of constants in process algebra ⋮ Unnamed Item ⋮ SOS formats and meta-theory: 20 years after ⋮ A general conservative extension theorem in process algebras with inequalities ⋮ An alternative formulation of operational conservativity with binding terms. ⋮ Unnamed Item ⋮ Rooted branching bisimulation as a congruence ⋮ Variable binding operators in transition system specifications ⋮ Lifting non-finite axiomatizability results to extensions of process algebras ⋮ Real time process algebra with time-dependent conditions ⋮ An axiomatic semantics for Esterel ⋮ A congruence rule format for name-passing process calculi ⋮ Coverability Synthesis in Parametric Petri Nets ⋮ Bisimilarity of open terms.

Uses Software

• Nuprl

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Structural operational semantics for weak bisimulations
• Transition system specifications with negative premises
• Recursive process definitions with the state operator
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Higher-level synchronising devices in Meije-SCCS
• Substitution revisited
• Model theory.
• A calculus of mobile processes. II
• Structured operational semantics and bisimulation as a congruence
• A theory of communicating processes with value passing
• A fully abstract denotational model for higher-order processes
• The lazy lambda calculus in a concurrency scenario
• The algebra of timed processes, ATP: Theory and application
• A general conservative extension theorem in process algebras with inequalities
• An operational semantics for timed CSP
• Discrete time process algebra
• Proving congruence of bisimulation in functional programming languages
• \(Ntyft/ntyxt\) rules reduce to \(n\)tree rules
• An effective axiomatization for real time ACP
• Real time process algebra
• A lattice-theoretical fixpoint theorem and its applications
• Process Algebra
• The well-founded semantics for general logic programs
• Bisimulation can't be traced
• The meaning of negative premises in transition system specifications
• πI: A symmetric calculus based on internal mobility
• Axiomatising real-timed processes

This page was built for publication: A conservative look at operational semantics with variable binding