Intuitionistic Linear Logic and Partial Correctness
Kozen, Dexter; Tiuryn, Jerzy
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-based models. As a corollary we obtain a complete sequent calculus for inclusion and equivalence of regular expressions.
computer science; technical report
Previously Published As