Abstract:

I propose a new technique for hardware synthesis from higher-order
functional languages with imperative features based on Reynolds's
Syntactic Control of Interference. The affine type system is useful for
managing the thorny issue of sharing in 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. Based on this
theoretical foundation we introduce a new ANSI C to hardware compiler
and we discuss some methodological issues regarding the role of higher
order programming languages in hardware design.