Convolution as a Unifying Concept
- Submitting institution
-
The University of Surrey
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 9025839_1
- Type
- D - Journal article
- DOI
-
10.1145/2874773
- Title of journal
- ACM Transactions on Computational Logic
- Article number
- -
- First page
- 1
- Volume
- 17
- Issue
- 3
- ISSN
- 1529-3785
- Open access status
- Out of scope for open access requirements
- Month of publication
- -
- Year of publication
- 2016
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
-
- Research group(s)
-
-
- Citation count
- 1
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- Over the years, many different models (traces, relations, matrices, automata, etc) have been developed to characterise computation. This international collaboration develops a unifying algebraic framework for these models based on functions from semigroups to quantales and a technique for lifting the "multiplication" operator using the notion of convolution. This captures many different computation models and gives rise to a generic Hoare logic. The significance of this work is that it forms the basis for mechanisation tools for separation logic, substructural logics, and interval logics implemented in the Isabelle theorem prover. These have all been the subject of more recent publications.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -