Substructural logic and partial correctness
Dexter C. Kozen, Jerzy Tiuryn · ACM Transactions on Computational Logic · 2003
We formulate a noncommutative sequent calculus for partial correctness that subsumes propositional Hoare Logic. Partial correctness assertions are represented by intuitionistic linear implication. We prove soundness and completeness over relational and trace models. As a corollary, we obtain a complete sequent calculus for inclusion and equivalence of regular expressions.