Home

Compositional type systems for stack-based low-level languages

Compositional type systems for stack-based low-level languages
by Ando Saabas and Tarmo Uustalu, appearing in Proceedings of the 12th Computing: The Australasian Theroy Symposium - 2006.

It is widely believed that low-level languages with jumps must be difficult to reason about by being inherently non-modular. We have recently argued that this in untrue and proposed a novel method for developing compositional natural semantics and Hoare logics for low-level languages and demonstrated its viability on the example of a simple low-level language with expressions (Saabas & Uustalu 2005). The central idea is to use the implicit structure of finite disjoint unions present in low-level code as an (ambiguous) phrase structure. Here we apply our method to a stack-based language and develop it further. We define a compositional natural semantics and Hoare logic for this language and go then on to show that, in addition to Hoare logics, one can also derive compositional type systems as weaker specification languages with the same method. We describe type systems for stack-error freedom and secure information flow.

I encountered the article while researching compositional type systems. I would like to hear people's thoughts about this article and compositional type-systems in general (are they interesting, esoteric, mundane?).

By cdiggins at 2007-09-13 12:19 | Type Theory | other blogs | 8993 reads

Comment viewing options

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

References/definitions of "Compositional Type System"?

It sounds, just from the name, much like Cliff Click's work on combining analyses in compiler analysis/optimization -- in that context, it's much like slapping a pile of lattices together to get a bigger lattice (i.e., propagate constants AND null/not AND types AND lock state AND relation to array bounds AND value numbers, all at once -- you get a better answer).

How is this work different from what goes on in Java (bytecode-to-native) compilers already? They do quite a lot of type analysis (though all the ones I know of translate the bytecodes into SSA-like representations), and have for some time.

By dr2chase at Thu, 2007-09-13 14:28 | login or register to post comments

Compositional type inference

There is a reference to compositional type-inference in the paper: The Essence of Principal Typings by J.B.Wells.

Principal typings allow compositional type inference, where the procedure of finding types for a term uses only the analysis results for its immediate sub-fragments, which can be analyzed independently in any order. Compositionality helps with such things as performing separate analysis of program modules.

Perhaps this is connected. I was assuming that type-system with compositional type inference could be called a compositional type system. So the term applied to all type-system that had principal typings (and perhaps more).

How is this work different from what goes on in Java (bytecode-to-native) compilers already?

That is a good question, I don't know.

By cdiggins at Thu, 2007-09-13 14:58 | login or register to post comments

That's different from Cliff's work

That's a different kind of compositional that Cliff's work, I think. (Cliff's stuff is difficult to understand even when you work in the field.)

By dr2chase at Fri, 2007-09-14 00:17 | login or register to post comments

Typo

That's Tarmo Uustalu :)

By Scott Graves at Thu, 2007-09-13 20:25 | login or register to post comments

Thanks.

Thanks.

By cdiggins at Fri, 2007-09-14 03:14 | login or register to post comments