LFCS Seminar: Tuesday, 7 February - George Kaye

Speaker:   George Kaye

Title:          A compositional theory of digital circuits  

Abstract: 

A syntax is compositional if complex components can be constructed out

simpler ones on the basis of their interfaces, without inspecting

their internals. Digital circuits, despite having been studied for

nearly a century and used at scale for about half that time, have until

recently evaded a fully compositional theoretical understanding.

The sticking point has been the need to avoid feedback loops that bypass

memory elements, the so called `combinational feedback' problem.

This requires examining the internal structure of a circuit,

defeating compositionality.

While there was previous work on remedying this theoretical

shortcoming by showing how digital circuits can be presented

compositionally as morphisms in a freely generated Cartesian traced

(dataflow) category, it was informal and emphasised certain

methodological points at the cost of mathematical clarity and

organisation. In this talk, we will give a new, more direct,

presentation in which syntax and semantics are neatly separated. We

will first detail how the semantics of digital circuits can be

interpreted as a certain class of stream functions, before presenting

an equational theory with which one can reason intuitively about

circuits.