BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Geometry of Synthesis: Semantics-directed hardware compilation - D
 an Ghica\, University of Birmingham School of Computer Science
DTSTART:20100610T130000Z
DTEND:20100610T140000Z
UID:TALK25152@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:The problem of synthesis of gate-level descriptions of digital
  circuits from behavioural specifications written in higher-level programm
 ing languages (hardware compilation) has been studied for a long time\, ye
 t a definitive solution has not been forthcoming. In this talk I will desc
 ribe a new technique based on recent advances in programming language theo
 ry: affine type systems\, monoidal categories and game semantics. We argue
  that one of the major obstacles in the way of a useful and mature hardwar
 e 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 m
 odel of affine higher-order type systems. Game semantics can provide inter
 pretations for common language constants which are concretely representabl
 e in this setting\, for both synchronous and asynchronous digital circuits
 . The key issue of sharing of resources and the additional structure requi
 red will also be addressed using game-semantic techniques. We illustrate t
 hese theoretical considerations with a prototype compiler from Syntactic C
 ontrol of Interference (an affine dialect of Idealised Algol) into digital
  circuits. 
LOCATION:Small Lecture Room\, Microsoft Research\, Roger Needham Building\
 , 7 J J Thomson Avenue\, Cambridge CB3 0FB
END:VEVENT
END:VCALENDAR