Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2001 | 10.1109/LICS.2001.932502 | LICS |
Keywords | Field | DocType |
partial correctness,linear logic,complete sequent calculus,intuitionistic linear logic,propositional hoare logic,gentzen-style sequent calculus,trace model,trace-based model,noncommutative intuitionistic linear logic,regular expression,noncommutative intuitionistic,calculus,computer science,technical report,completeness,soundness,hoare logic,ambient intelligence,regular expressions,algebra,formal logic,sequent calculus | Discrete mathematics,Natural deduction,Proof calculus,Noncommutative logic,Sequent,Linear logic,Many-valued logic,Cut-elimination theorem,Mathematics,Curry–Howard correspondence | Conference |
ISSN | Citations | PageRank |
1043-6871 | 1 | 0.39 |
References | Authors | |
7 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Dexter C. Kozen | 1 | 5108 | 912.56 |
| Jerzy Tiuryn | 2 | 1210 | 126.00 |