Rencontre, 5 mai 2022

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 safe-normal function algebra, and we identify proof theoretical constraints, inspired by ICC, to characterise the polynomial-time 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 non-wellfounded proof systems to capture non-uniform 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 lambda-terms. This machine is based on implementations of strong call-by-need evaluation, and is able to exploit that convertibility is closed by context: to prove that f x is convertible with f y when f is a constant, it it enough to prove that x and y are convertible. However, it is sometimes more efficient to unfold f 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)

Invited talk: Linear logic with fixpoints from a Curry-Howard perspective.

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.