Kozen, Dexter2007-04-232007-04-231999-07http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR99-1760https://hdl.handle.net/1813/7414We 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.164914 bytes142162 bytesapplication/pdfapplication/postscripten-UScomputer sciencetechnical reporttechnical report