Substructural Logics of Programs

Substructural logics seem to provide a natural framework formalizing reasoning about programs, as witnessed by R-models of the Lambek calculus, for instance. Indeed, Pratt's action algebras are expansions of residuated idempotent semirings, structures naturally arising in algebraic semantics for substructural logics. Kozen and Tiuryn have introduced a substructural logic tailored to formalize reasoning about correctness of programs (Substructural Logic and Partial Correctness, ACM Trans. Comput. Logic, 2003), sound and complete with respect to a semantics based on binary relations. In this talk, we prove that Kozen and Tiuryn's logic embeds into an expansion of *-continuous action algebras with a pair of adjoint test-like operators.