Geometry of synthesis: a structured approach to VLSI design

We propose a new technique for hardware synthesis from higherorder 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. Categories and Subject Descriptors F.3.2 [Semantics of Programming Languages]: Denotational semantics; B.7.1 [Types and Design Styles]: VLSI General Terms Design, Languages, Theory Keywords Syntactic Control of Interference, Geometry of Interaction, game semantics, synthesis

• Type: Conference
• Year: 2007
• Where: POPL
• Authors: Dan R. Ghica
• Keywords: General Terms Design, POPL 2007, Programming Languages, Syntactic Control, Theory Keywords Syntactic