A compositional theory of digital circuits: Part III

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

• George Kaye (University of Birmingham)
• Thursday 13 October 2022, 14:00-15:00
• LG23, SoCS.

If you have a question about this talk, please contact Anupam Das.

[This is a continuation of the last two weeks’ Lab Lunches.]

A theory is compositional if complex components can be constructed out of simpler ones on the basis of their interfaces, without inspecting their internals. Digital circuits, despite being 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 are not guarded by a memory element (a ‘delay’): this requires examining the internal structure of a circuit, defeating compositionality.

Recent work remedied this theoretical shortcoming by showing how digital circuits can be presented compositionally as morphisms in a freely generated Cartesian traced category: as a result circuits could be reasoned about equationally. However, this work was presented informally, and, crucially, was still not complete for circuits with non-delay-guarded feedback. Our work seeks to formalise the semantics of the syntactic circuit morphisms as a certain class of functions on streams, and to introduce the ‘missing equations’. This ensures that our model is fully abstract: the equational model and the semantic model are in perfect agreement.

[NB: this is a physical-only whiteboard talk]

This talk is part of the Lab Lunch series.

This talk is included in these lists:

• LG23, SoCS
• Lab Lunch

Note that ex-directory lists are not shown.