University of Cambridge > > Microsoft Research Cambridge, public talks > Geometry of Synthesis: Semantics-directed hardware compilation

Geometry of Synthesis: Semantics-directed hardware compilation

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

The problem of synthesis of gate-level descriptions of digital circuits from behavioural specifications written in higher-level programming languages (hardware compilation) has been studied for a long time, yet a definitive solution has not been forthcoming. In this talk I will describe a new technique based on recent advances in programming language theory: affine type systems, monoidal categories and game semantics. We argue that one of the major obstacles in the way of a useful and mature hardware compiler is the lack of a well defined function interface model, i.e. a canonical way in which functions can communicate with their arguments. We will show how digital circuits exhibit an inherent structure which is a model of affine higher-order type systems. Game semantics can provide interpretations for common language constants which are concretely representable in this setting, for both synchronous and asynchronous digital circuits. The key issue of sharing of resources and the additional structure required will also be addressed using game-semantic techniques. We illustrate these theoretical considerations with a prototype compiler from Syntactic Control of Interference (an affine dialect of Idealised Algol) into digital circuits.

This talk is part of the Microsoft Research Cambridge, public talks series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2023, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity