Flexible Coinductive Definitions by Inference Systems

Francesco Dagnino

University of Genoa




Abstract: Inference systems are a widespread framework, used to define possibly recursive predicates by means of inference rules. They allow both inductive and coinductive interpretations that are fairly well-studied. However, there are cases where none of them provides the expected meaning. Inference systems with corules have been recently introduced precisely to address this issue. Indeed, by means of corules, it is possible to select an interpretation lying between the inductive and the coinductive one, thus providing more flexibility.

In this talk, I will introduce inference systems with corules, presenting their proof-theoretic and fixed point semantics and the associated proof principle. Then, I will show how standard inductive and coinductive interpretations can be recovered by specific choices of corules, and, finally, I will discuss how corules can be used to define big-step operational semantics modelling infinite computations.