Zeta Functions and the (Linear) Logic of Markov Processes

In a series of papers, the author introduced models of linear logic known as "Interaction Graphs". These models generalise Girard's various geometry of interaction constructions, providing a unifying framework for those. In this work, we exhibit how these models can be understood mathematically through a cocycle property satisfied by zeta functions of dynamical systems. Focussing on probabilistic models, we then explain how the notion of graphings used in the models captures a natural class of Markov processes. We further extend previous constructions to provide a model of second-order linear logic as a type system over the set of all (discrete-time) sub-Markov processes.