Geometry of synthesis

Abstract

We propose a new technique for hardware synthesis from higher-order functional languages with imperative features based on Reynolds's Syntactic Control of Interference . The restriction on contraction in the type system is useful for managing the thorny issue of sharing of physical circuits. We use a semantic model inspired by game semantics and the geometry of interaction, and express it directly as a certain class of digital circuits that form a cartesian, monoidal-closed category. A soundness result is given, which is also a correctness result for the compilation technique.