Talk "Codensity Lifting: a Unified Framework for Observations in Process Theory"

by Ichiro Hasuo

Tue, 14 January 2020 at 04:30 pm in Massa Marittima, Italy

Joint work with: Yuichi Komorida, Shin-ya Katsumata, Nick Hu, Bartek Klin, Clemens Kupke, Jurriaan Rot

Abstract: Lifting an endofunctor along a fibration is a central construction in many problems such as fibrational modal logic, fibrational modeling of behavioral equivalence and behavioral metric, etc. Codensity lifting, introduced in [Katsumata, Sato and Uustalu, LMCS’18] as a variation of \top\top-lifting, is a general method for such functor lifting. Codensity lifting is known to yield a number of concrete liftings known in the literature (including the so-called abstract Kantorovich lifting introduced in [Baldan, Bonchi, Kerstan and Koenig, LMCS’18]); its formalization in terms of “compatible observations” is not only conceptually natural but also enables the construction to collaborate nicely with other common gadgets in theoretical computer science. In this talk, after introducing codensity lifting using an analogy that is very much like in “topology via logic,” I introduce two recent works of ours about its use in foundational problems in process theory: game characterization of bisimilarity-like notions [Komorida, Katsumata, Hu, Klin, H., LICS’19] and expressivity of duality-based coalgebraic modal logics [Komorida, Katsumata, Kupke, Rot, H., ongoing].