My research activity lies at the intersection of three areas: mathematical logic, theoretical computer science and duality theory. I am particularly interested in the interconnections between them. Duality theory, initiated by mathematician M. H. Stone in 1936, provides a mathematical framework to study connections such as those between algebra and geometry, or observables and states, which abound both in the mathematics and physics world. When applied to logic, duality allows us to study the link between syntax and semantics. In theoretical computer science, the interplay between syntax and semantics is of central importance, as the two sides correspond to specification languages and computational states. The ability to move between these two worlds has often proved a useful tool. A prime example is Abramsky’s Domain Theory in Logical Form (Abramsky, 1991), bridging program logic and domain theory via Stone duality.
I pursue two main research directions. The first consists in developing and applying duality methods to more algorithmic areas of theoretical computer science, where duality has not yet played a role (or not until recently, at least). These include formal language theory and finite model theory. In particular, I am currently working on a structural/topological understanding of Rossman’s Equirank and Finite Homomorphism Preservation theorems (Rossman, 2005, 2008). An exciting challenge, in this respect, consists in combining the duality theoretic techniques with the categorical and comonadic approach recently put forward by Abramsky, Dawar and their collaborators.
The second aims at studying logics with quantifiers using Stone-type dualities. While duality has proved a powerful tool in the study of propositional logics, many applications require first-order or higher-order logics. Although some notions of duality for first-order logics, based on categorical semantics, have been proposed (Makkai, 1987), applications are few and far between. On the other hand, in recent works with several collaborators, a dual correspondence between quantification and a space-of-measures construction has started to emerge in the context of logic on words and finite model theory. See here or here. An interesting venue of research consists in providing a systematic understanding of quantifiers as dual to measures, and relate it to other approaches, such as compact abstract theories in positive model theory (Ben-Yaacov, 2003).
Finite model theory (FMT) is the specialisation of model theory to finite structures, and has been called “the logic of computer science” since in the latter field the basic models of computation are finite. Many classical results of model theory, such as the Compactness and Completeness theorems, fail when restricted to finite models. For this reason, FMT has developed independently from model theory and the research communities, as well as the techniques, are almost disjoint. FMT exemplifies a strand in the field of logic in computer science focussing on expressiveness and complexity (Power), as opposed to the one focussing on semantics and compositionality (Structure). In my Marie Curie project D-FINED (Duality for finite models) I aim to apply duality methods to bridge the gap between the semantics methods of model theory, and the combinatorial and complexity-theoretic methods of FMT, i.e., to relate Structure and Power.
This line of research naturally extends part of the work I carried out in my PhD thesis, concerning the link between semiring quantifiers in logic on (finite) words and spaces of finitely additive semiring-valued measures. An important tool there was a combination of duality theoretic and categorical methods, especially in the form of codensity monads (see here). Currently, I am working on combining duality techniques with the coalgebraic/comonadic approach to FMT put forward by Abramsky, Dawar et al. This includes the case of the pebbling comonad, the Ehrenfeucht-Fraïssé comonad and others. For more on game comonads, have a look at the Co-Wiki maintained by Tomáš Jakl.