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. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Benton, N. (2005). A typed, compositional logic for a stack-based abstract machine. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3780 LNCS, pp. 364–380). https://doi.org/10.1007/11575467_24
Mendeley helps you to discover research relevant for your work.