ReflectionsOnThePost-ModernStage

Speaker: Jun Inoue, PhD student

Part 1. Reasoning About Staged Programs

The most important use of staging is to write efficient programs that are nonetheless easy to understand and analyze. Paradoxically, however, little is known about how to check the correctness of staged code. In fact, virtually nothing is known about the multi-stage lambda calculus, apart from the mere existence of an axiomatic equational theory. By contrast, for the plain lambda calculus, we have an extensive understanding of the properties of equations provable in the axiomatic and denotational theories. These help programmers and language designers to avoid bugs and is a key ingredient for formal verification.

My Master's thesis is a first step towards developing the metatheory of multi-stage languages in that direction. I prove that staging annotations induce a homomorphism (wrt. beta equalities) on the multi-stage lambda calculus, which formally limits the effect that staging has on program semantics. I show how this result can be used to verify the staged power function. As a negative result, I show that staging is a non-conservative extension in the untyped CBV setting. This limits reasoning on multi-stage terms, but I show a supplementary proof rule based on a variant of applicative bisimulation that can make up for it in common cases.

Part 2. FPGA Offshoring

This part describes a prospective work, and hence will be brief. I would like to use multi-stage programming to generate hardware circuits to load and execute on an FPGA, to use it as a coprocessor. I believe this approach provides a tightly integrated, unified view of the host computation (i.e. which controls and directs circuit generation) and the FPGA computation. In this talk, I will describe the basic, existing approach to generating circuits from generated (Meta)OCaml code and explain how I plan to structure the overall FPGA programming system based on MetaOCaml.