University of Birmingham > Talks@bham > Lab Lunch > A compositional theory of digital circuits: Part II

A compositional theory of digital circuits: Part II

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

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

[This is a continuation of last week’s Lab Lunch.]

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on talks.cam from the University of Cambridge.