A Typed Logic for Stacks and Jumps
- Nick Benton
This note shows how one may define a program logic in the style of Floyd and Hoare for a simple, typed, stack-based, imperative language with unstructured control flow and local variables.
This note shows how one may define a program logic in the style of Floyd and Hoare for a simple, typed, stack-based, imperative language with unstructured control flow and local variables.