Non-wellfounded proof theory for fixed-point logics
Seminario: 4 luglio 2019 alle 14.30 in aula riunioni 4 piano.<br>
Speaker: Alexis Saurin<br>
Referente: Alberto Momigliano
Non-wellfounded and circular proofs are commonly used in fixed point logics. Being natural intermediate devices between semantics and traditional finitary proof systems, they are commonly found in completeness arguments, automated deduction, verification, etc. Their proof theory is surprisingly under-developed. In particular, little is known about the computational behavior of such proofs through cut elimination. Taking such aspects into account has unlocked rich developments at the intersection of proof theory and programming language theory. One would hope that extending this to infinitary calculi would lead, e.g., to a better understanding of recursion and corecursion in programming languages.
With such non-wellfounded proof systems, a global validity condition is required in order to preserve soundness of the logic. This condition is expressed as requiring that every non-wellfounded branch of the proof is inhabited by a "progressing thread".
In this talk, I will present a survey on the infinitary proof theory of μMALL∞ (ie multiplicative and additive linear logic extended with least and greatest fixed points), discussing recent results mostly related to the question of cut-elimination and productivity of computations on infinite objects. I will especially discuss the impact of a discrepancy between the sequential nature of sequent proofs and the parallel nature of those threads.
Alexis Saurin is a CNRS researcher at IRIF lab in Paris (CNRS and Université de Paris). He is a member of the pi.r2 INRIA project-team. His research investigates various aspects of the Curry-Howard correspondence, from the computational content of classical logic, to call-by-need and more recently the investigation of (co)induction in fixed points logics.