On a Universal Property of the Algebra of Contracts
Inigo Incer · Theory and applications of categories · 2024
We consider Stone algebras with a distinguished element e satisfying the identity e → x = ¬¬x for all elements x of the algebra.We provide an adjunction between the category of such algebras and that of Boolean algebras.This adjunction turns out to involve the concept of assume-guarantee contracts, which has numerous applications throughout engineering and computer science.