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 | 9444 reads
|
Browse archives
Active forum topics |
Recent comments
6 weeks 14 hours ago
6 weeks 18 hours ago
6 weeks 18 hours ago
28 weeks 1 day ago
32 weeks 3 days ago
34 weeks 1 day ago
34 weeks 1 day ago
36 weeks 5 days ago
41 weeks 3 days ago
41 weeks 3 days ago