Effect Algebras, Girard Quantales and Complementation in Separation Logic

Autor:	Peter Höfner, Callum Bannister, Georg Struth
Rok vydání:	2021
Předmět:	Lift (mathematics) Pure mathematics Negation Mathematics::Category Theory Assertion Separation logic Abelian group Convolution Mathematics
Zdroj:	Relational and Algebraic Methods in Computer Science ISBN: 9783030887001 RAMiCS
DOI:	10.1007/978-3-030-88701-8_3
Popis:	We study convolution and residual operations within convolution quantales of maps from partial abelian semigroups and effect algebras into value quantales, thus generalising separating conjunction and implication of separation logic to quantitative settings. We show that effect algebras lift to Girard convolution quantales, but not the standard partial abelian monoids used in separation logic. It follows that the standard assertion quantales of separation logic do not admit a linear negation relating convolution and its right adjoint. We consider alternative dualities for these operations on convolution quantales using boolean negations, some old, some new, relate them with properties of the underlying partial abelian semigroups and outline potential uses.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::28fd208f2c63b59f9cc584e7b0afa9da https://doi.org/10.1007/978-3-030-88701-8_3 Zobrazit plný text záznamu