Speaker: Ross Duncan, University of Strathclyde Time and location: 15:15, EM 3.07 Abstract: Diagrams are widely used in science and engineering; well known examples include electronic circuit diagrams, Feynman diagrams, proof-nets, petri-nets, and countless others. All these diagrams share the same basic features because they are all presentations of monoidal categories — one of...

Read more →

Abstract: We have developed a hardware accelerator for motion planning, a critical operation in robotics. I will present the microarchitecture of our accelerator and describe a prototype implementation on an FPGA. Experimental results show that, compared to the state of the art, the accelerator improves performance by three orders of magnitude and improves power...

Read more →

Distributed systems play a crucial role in modern infrastructure, but are notoriously difficult to implement correctly. This difficulty arises from two main challenges: (a) correctly implementing core system components (e.g., two-phase commit), so all their internal invariants hold, and (b) correctly composing standalone system components into functioning trustworthy applications (e.g., persistent storage built on...

Read more →

We show that, given a word equation over a finitely generated free group (or semigroup), the set of all solutions in reduced words forms an EDT0L language. In particular, it is an indexed language in the sense of Aho. This is joint work with Murray Elder and Volker Diekert.

Read more →

Logic programming, that is Horn Clause Logic equipped with a resolution mechanism, provides an expressive framework for first order proving with computational advantages over alternative approaches. Traditionally, resolution mechanisms employ full unification. Recently, however, attention was given to type-theoretic interpretation of logic programming with the focus on universal fragment of Horn Clause Logic where...

Read more →