User loginNavigation |
A Typed, Compositional Logic for a Stack-Based Abstract Machine
A Typed, Compositional Logic for a Stack-Based Abstract Machine. Nick Benton. MSR-TR-2005-84. June 2005.
We define a compositional program logic in the style of Floyd and Hoare for a simple, typed, stack-based abstract machine with unstructured control flow, global variables and mutually recursive procedure calls. Notable features of the logic include a careful treatment of auxiliary variables and quantification and the use of substructural typing to permit local, modular reasoning about program fragments. Semantic soundness is established using an interpretation of types and assertions defined by orthogonality with respect to sets of contexts. By Ehud Lamm at 2005-07-02 09:14 | Implementation | Semantics | Type Theory | other blogs | 9371 reads
|
Browse archives
Active forum topics
|
Recent comments
15 weeks 1 day ago
19 weeks 3 days ago
21 weeks 18 hours ago
21 weeks 18 hours ago
23 weeks 5 days ago
28 weeks 2 days ago
28 weeks 3 days ago
28 weeks 6 days ago
28 weeks 6 days ago
31 weeks 4 days ago