Rencontre, May 5, 2022
Le lendemain, vendredi 6 mai, se tiendra une journée du projet ANR Reciprog, à Lyon, son programme est ici.
Programme
 10:30 – 12:00

Gianluca Curzi (Università di Torino)Invited talk: Cyclic implicit complexity
Circular (or cyclic) proofs have received increasing attention in recent years, and have been proposed as an alternative setting for studying (co)inductive reasoning. In particular, now several type systems based on circular reasoning have been proposed. However, little is known about the complexity theoretic aspects of circular proofs, which exhibit sophisticated loop structures atypical of more common ‘recursion schemes’. This talk attempts to bridge the gap between circular proofs and implicit computational complexity (ICC). Namely we introduce a circular proof system based on Bellantoni and Cook’s famous safenormal function algebra, and we identify proof theoretical constraints, inspired by ICC, to characterise the polynomialtime and elementary computable functions. Along the way we introduce new recursion theoretic implicit characterisations of these classes that may be of interest in their own right. Finally, we study nonwellfounded proof systems to capture nonuniform complexity classes such as P/poly.
 14:00 – 15:00

Nathanaëlle Courant (INRIA)Invited talk: Testing convertibility in parallel
In this talk, I will present a machine for testing the convertibility of lambdaterms. This machine is based on implementations of strong callbyneed evaluation, and is able to exploit that convertibility is closed by context: to prove that
f x
is convertible withf y
whenf
is a constant, it it enough to prove thatx
andy
are convertible. However, it is sometimes more efficient to unfoldf
to prove convertibility, for instance if it does not use its argument. Our machine solves both convertibility problems in parallel while sharing computations, and stops as soon as it is able to conclude about the initial problem.  15:30 – 16:30

Farzad Jafarrahmani (IRIF)
I first, briefly, present the syntax of MuLL which is an extension of David Baelde’s MuMALL (multiplicative and additive linear logic with least and greatest fixpoints) with exponentials. Then we will study the categorical model of Mu LL and provide two concrete models of MuLL based and REL (sets and and relation) and NUTS (non uniform totality spaces) which are sets equipped with a notion of totality and a relation preserving it. Then we will study a polarized version of muLL, and will try to develop a calculus based on this polarized version, called mu LLP. We equip this language with a deterministic reduction semantics as well as a denotational semantics based on NUTS. Finally, We prove an adequacy result between these operational and denotational semantics, from which we derive a normalization property for mu LLP thanks to the properties of the totality interpretation.
This presentation is based on joint work with Thomas Ehrhard and Alexis Saurin.