[TYPES] Paper: A compositional natural semantics and Hoare logic for low-level languages

[Tarmo Uustalu]

Dear TYPES subscribers,

We'd like to announce a new paper 

A compositional natural semantics and Hoare logic for low-level languages

http://cs.ioc.ee/~tarmo/papers/sos05.pdf

to appear in the ENTCS volume for SOS 2005.

This is a new approach to semantic and logic descriptions of
low-level languages (where a piece of code is a flat set of labelled
instructions). The key idea is to use finite non-overlapping unions of
pieces of code as a phrase structure.  Although this may at first look
like a very uninteresting phrase structure, it is actually perfectly
good both metatheoretically and from the practical software technogy
point of view. A salient feature is compositional compilability of
high-level program proofs.

Best wishes,

Ando Saabas, Tarmo Uustalu