JavaScript is disabled for your browser. Some features of this site may not work without it.
On Hoare Logic, Kleene Algebra, and Types

Author
Kozen, Dexter
Abstract
We show that propositional Hoare logic is subsumed by the type calculus of typed Kleene algebra augmented with subtypes and typecasting. Assertions are interpreted as typecast operators. Thus Hoare-style reasoning with partial correctness assertions reduces to typechecking in this system.
Date Issued
1999-07Publisher
Cornell University
Subject
computer science; technical report
Previously Published As
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR99-1760
Type
technical report