Home

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.

Also related to PCC, TAL etc.

By Ehud Lamm at 2005-07-02 09:14 | Implementation | Semantics | Type Theory | other blogs | 9995 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Just sticking this in

This makes me think about a few papers I read a while back that I don't think have been mentioned on LtU before. They are various papers by Atsushi Ohori (http://www.jaist.ac.jp/~ohori/research/list.html). The notable aspect is the more "grungy" use of the Curry-Howard correspondence (or alternatively the much higher level view of typically more "grungy" aspects of language implementation). I imagine there are some readers who think the CH correspondence is all well and nice, but don't really see how it would be used. With titles such as "Register Allocation by Proof Transformation", this might provide some light.

By Derek Elkins at Sat, 2005-07-02 14:13 | login or register to post comments

There are also various kinds

There are also various kinds of error that are, at least
a priori, possible in the dynamic semantics: stack underflow, wild jumps and
type errors. We deal with these issues by defining a fairly simple type system
that rules out erroneous behaviour, and defining assertions relative to typed
programs.

 

It is interesting that this paper addresses the issues of
the reliability of register machines by defining a type checked intermediate
abstract machine (ie a virtual machine). The reliability of register machines
issue was addressed in a recent post and Discussion where we
proposed the use of a backtracking VM: Lewis.

By Hank Thediek at Sat, 2005-07-02 14:15 | login or register to post comments