Computation-by-Interaction for Structuring Low-Level Computation
Ulrich Schöpp · 2014
In game semantics and related approaches to programming language semantics, computation is modelled by interaction dialogues. Such models of computation have been used to guide the implementation of programming languages. The idea is to implement interaction dialogues directly and thus realise computation by interaction. In this thesis we study computation-by-interaction as an approach to structuring low-level computation. We capture semantic structure of interactive computation in terms of a typed λ-calculus int and study its use for organising low-level computation. We start by considering the practical application of int as a language for low-level programming. Next we show that it allows fine-grained control over space usage by using it to characterise the complexity class of the functions computable in logarithmic space. We then show how int can be used to translate functional languages with call-by-name and call-by-value evaluation strategy to a low-level language. We observe that the translation for call-by-name is closely related to standard compilation techniques, namely cps-translation and defunctionalization. We use the translation of call-by-value as an example to illustrate the use of the structure identified by int for non-trivial reasoning about low-level programs.