Convolution as a Unifying Concept

DOI10.1145/2874773MaRDI QIDQ5277916zbMATH OpenOpenAlexWikidataFDO

Authors Brijesh Dongol, Ian Hayes, Georg Struth

Publication date 12 July 2017

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2874773

zbMATH Keywords

convolutionformal power seriesconcurrencysemigroupsquantalesformal semanticssystems verificationHoare logicsinterval logicsseparation logics

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Quantales (06F07)

Recommendations

• On the relation between concurrent separation logic and concurrent Kleene algebra
• Concurrent separation logic and operational semantics
• Revisiting concurrent separation logic
• A semantics for concurrent separation logic
• CONCUR 2004 - Concurrency Theory
• The essence of higher-order concurrent separation logic
• The inner and outer algebras of unified concurrency
• Separation logic and concurrency
• Precision and the conjunction rule in concurrent separation logic
• Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency

Cites work

• scientific article; zbMATH DE number 3915644 (Why is no real title available?)
• scientific article; zbMATH DE number 3735177 (Why is no real title available?)
• scientific article; zbMATH DE number 3751225 (Why is no real title available?)
• scientific article; zbMATH DE number 3497806 (Why is no real title available?)
• scientific article; zbMATH DE number 1507210 (Why is no real title available?)
• scientific article; zbMATH DE number 3366846 (Why is no real title available?)
• A language of specified programs
• A program construction and verification tool for separation logic
• An algebra of hybrid systems
• BI as an assertion language for mutable data structures
• Boolean Algebras with Operators
• Boolean Algebras with Operators. Part I
• Classical relevant logics. I
• Concurrent Kleene algebra and its foundations
• Convolution as a Unifying Concept
• Duration calculus. A formal approach to real-time systems.
• Handbook of weighted automata
• Isabelle/HOL. A proof assistant for higher-order logic
• Kripke models for linear logic
• On closed categories of functors
• On locality and the exchange law for concurrent processes
• On the foundations of combinatorial theory I. Theory of M�bius Functions
• Parallel programming: An axiomatic approach
• Partition Theorems for Spaces of Variable Words
• Power structures
• Quantales and Temporal Logics
• Semantics for relevant logics
• The Logic of Bunched Implications
• The equational theory of pomsets
• Varieties of complex algebras
• Verifying properties of parallel programs
• Views, compositional reasoning for concurrent programs

Cited in

(8)

• Unifying Operational Weak Memory Verification: An Axiomatic Approach
• A nominal approach to probabilistic separation logic
• Convolution and concurrency
• Convolution as a Unifying Concept
• Effect algebras, Girard quantales and complementation in separation logic
• Convolution algebras: relational convolution, generalised modalities and incidence algebras
• A program construction and verification tool for separation logic
• Catoids and modal convolution algebras

Describes a project that uses

Uses Software

• Isabelle/HOL

This page was built for publication: Convolution as a Unifying Concept

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