The laws of Occam programming

DOI10.1016/0304-3975(88)90049-7MaRDI QIDQ2640348zbMATH OpenOpenAlexFDO

Authors A. W. Roscoe, Tony Hoare

Publication date 1988

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(88)90049-7

zbMATH Keywords

algebraic semantics of parallel processesOccam

Mathematics Subject Classification ID

Theory of programming languages (68N15) Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Semantics in the theory of computing (68Q55)

Review text

The authors describe an equational axiomatization of the semantics of OCCAM. They show that WHILE-free programs have a normal form, such that two programs are semantically equivalent if and only if their normal forms are syntactically equivalent. This shows that their equational axiomatization, together with an induction axiom, is a sound and complete proof system for proving the equivalence of OCCAM programs. The paper is very clearly written.

Recommendations

• scientific article; zbMATH DE number 43800
• Laws of programming
• Generic models of the laws of programming
• Coding Ockham's Razor
• The laws of programming unify process calculi
• scientific article; zbMATH DE number 41788
• Laws of programming for references
• A practical theory of programming

Cites work

• A Proof System for Communicating Sequential Processes
• scientific article; zbMATH DE number 3898198 (Why is no real title available?)
• scientific article; zbMATH DE number 3902016 (Why is no real title available?)
• scientific article; zbMATH DE number 3902017 (Why is no real title available?)
• scientific article; zbMATH DE number 3972168 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 3794037 (Why is no real title available?)
• Laws of programming
• Programming as a Discipline of Mathematical Nature

Cited in

(23)

• A proof system for communicating processes with value-passing
• An algebraic hardware/software partitioning algorithm
• Proof systems for message-passing process algebras
• On fairness notions in distributed systems. I: A characterization of implementability
• Unifying theories of reactive design contracts
• A formal model for a hybrid programming language
• Towards a modeling language for cyber-physical systems
• Formal sequentialization of distributed systems via program rewriting
• A new roadmap for linking theories of programming
• From safety critical Java programs to timed process models
• Coding Ockham's Razor
• Formal communication elimination and sequentialization equivalence proofs for distributed system models
• Interfaces between languages for communicating systems
• UTP, \textsf{\textit{Circus}}, and Isabelle
• Linking formal methods in software development. A reflection on the development of rCOS
• Communicating processes with value-passing and assignments
• On concurrent program algebra and demonic automata
• A theory of software product line refinement
• Receptive process theory
• A new use of an automated reasoning assistant: Open questions in equivalential calculus an the study of infinite domains
• Correct hardware synthesis
• Revisiting sequential composition in process calculi
• The projection of systolic programs

This page was built for publication: The laws of Occam programming

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2640348)