I just came back from ACT after missing it for three years; it was great to see so many familiar faces and many new ones too!
I was lucky to have three works featured in the programme, and even luckier to have my coauthors present them.
-
David Jaz Myers talked about our joint paper Compositionality of Lyapunov functions via assume-guarantee reasoning. The work stems from the idea that once we have a categorical treatment of systems, then we also know how to do logic for them---just look at fibrations! Specifically, if we think of systems as objects of certain 2-algebras, where the 2-algebraic structure describes their compositionality, then the resulting framework is a logic with the same compositionality as the system we predicate about. This is in fact an old idea of mine.
This is put to good use in our paper, where we show that Moore machines of predicates are a very easy and effective framework for assume-guarantee reasoning. With a bit of cleverness, we also show how Lyapunov certificates for the stability of ODEs equilibria fit the bill.
-
Anny Beatriz Azevedo presented Algorithmic and Extremal Obstructions Through the Language of Cohomology , a work joint with Benjamin Merlin Bumpus, Daniel Rosiak, James Fairbanks, and me. She gave a really clean and clear talk, presenting the material so well: you could tell by the number of questions!
-
Nathaniel Virgo presented on-going work with me, Martin Biehl, and Manuel Baltieri. Their talk was titled The universal property of possibilistic Bayesian update and is basically a follow-up to A "good regulator theorem" for embodied agents and A Bayesian Interpretation of the Internal Model Principle. There we revisit the good regulator theorem and a formal correspondence between subsets \(R \subseteq X \times Y\) on the state space of coupled controller-plant machines, and certain `model-like' maps \(\lambda R: X \to PY\) from the controller to the power set of the plant states. Such maps present every controller state as encoding a belief about the plant state, with beliefs evolving coherently with the controller dynamics and compatibly with the plant's.
It is thus natural to wonder if such a map \(\lambda R\) is in fact a map of systems, so that we can see \(PY\) as a proper system whose evolution encodes some kind of inference dynamics.
That is indeed the case! Working `behaviourally', we can construct \(PY\) in some examples of interest and interpret its dynamics to be precisely a possibilistic (i.e. non-probabilistic) version of Bayesian update.
I'm really excited about this work, which is also rooted in categorical logic ideas deployed in the context of categorical systems theory. When we have a preprint ready, I will make sure to blog about it. For now, you can check Nathaniel's abstract.
Besides these talks, I enjoyed many other presentations. Here's a non-exhaustive list.
- Jules Hedges and Dylan Braithwaite had talks about their efforts at Glaive to create a programming language where types are containers (these being the syntactic counterpart of polynomial functors). Jules' talk was actually a demo: they can already run some fairly simple yet impressive programs. They blogged about it here. Dylan's talk was much more theory-heavy, as he is in the process of axiomatizing the internal language of \(\mathsf {Poly}\), a truly ambitious effort.
- Joe Moeller talked about categorical Lyapunov theory in two very engaging talks, probably my favourite at the conference. One talk's abstract is here and the other is here but you can also check the paper.
- Andrés Ortiz-Muñoz wrote an intriguing paper on DNA structures as arrows in a rigid category---it certainly made for beautiful slides!
- Kristopher Brown had a paper on formalizing logical expressivism, a philosophical framework for logic where inferences come first and rules come later.
We also had a community session about the impact of LLMs on the conference, which was a great chance to probe the mood of the community about the topic and to start acting on the problem. The general sentiment seems to be that LLMs can be very helpful with some of the tasks involved in redacting a paper or a review (search for literature, generate figures, check for typos and obvious flaws, etc.), but there is some division on whether more than that is acceptable.
I split off my thoughts about that in another post.
You can comment on this post on Mastodon.