### Abstract

Partial Semigroups are relevant to the foundations of quantum mechanics and combinatorics as well as to interval and separation logics. Convolution algebras can be understood either as algebras of generalised binary modalities over ternary Kripke frames, in particular over partial semigroups, or as algebras of quantale-valued functions which are equipped with a convolution-style operation of multiplication that is parametrised by a ternary relation. Convolution algebras provide algebraic semantics for various substructural logics, including categorial, relevance and linear logics, for separation logic and for interval logics; they cover quantitative and qualitative applications. These mathematical components for partial semigroups and convolution algebras provide uniform foundations from which models of computation based on relations, program traces or pomsets, and verification components for separation or interval temporal logics can be built with little effort.

### License

BSD License

### Topics

- Mathematics/Algebra

### Session PSemigroupsConvolution

- Partial_Semigroups
- Partial_Semigroup_Models
- Quantales
- Binary_Modalities
- Unary_Modalities
- Partial_Semigroup_Lifting

## Cite

×

PSemigroupsConvolution-AFP

    @article{PSemigroupsConvolution-AFP,
      author  = {Brijesh Dongol and Victor B. F. Gomes and Ian J. Hayes and Georg Struth},
      title   = {Partial Semigroups and Convolution Algebras},
      journal = {Archive of Formal Proofs},
      month   = {June},
      year    = {2017},
      note    = {\url{https://isa-afp.org/entries/PSemigroupsConvolution.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Jun 13, 2017 : Isabelle2016-1