Intuitionistic linear logic and partial correctness
Dexter C. Kozen, Jerzy Tiuryn · 2002
We formulate a Gentzen-style sequent calculus for partial correctness that subsumes propositional Hoare logic. The system is a noncommutative intuitionistic linear logic. We prove soundness and completeness over relational and trace models. As a corollary, we obtain a complete sequent calculus for the inclusion and equivalence of regular expressions.