TBA

The aim of this talk is to combine profinite methods used in automata theory and models of the λ-calculus to obtain a notion of profinite λ-term. Profinite words provide a way to speak about limiting behavior of finite words with respect to deterministic automata. In order to connect this notion of profiniteness to the λ-calculus, we consider higher-order automata which can process arbitrary simply-typed λ-terms as their input. Existing notions of automata on words and trees are then obtained as special cases.

Our main contribution is the study of the notion of parametric λ-term in the sense of Reynolds. We establish a link with profinite words in the cartesian closed category of finite sets and functions, which corresponds to deterministic automata. We prove that in this setting, the notion of parametric λ-term essentially coincides with the classical notion of profinite word.

In this talk, I'll explain how to extend cut-elimination results for non-wellfounded muMALL (typically BDS 2016) to nwf muLL by exploiting the encoding of the exponential modalities in muMALL. A notable fact is that the extension can use the original cut-elimination proof almost entirely as a black-box (and therefore can be adapted seen as parametric with respect to other criteria – be there more expressive or on the contrary more restrictive than the straight-thread validity condition): the extension essentially relies on standard results and reasonings from infinitary rewriting in the spirit of the so-called dutch school.

I'll also discuss some facts about the fixed-point encoding of the exponentials and its shortcomings as well as, extension to other fixed-point sequent calculi, typically nwf muLK and muLJ.

This talk investigates the question of denotational invariants of non-wellfounded proofs of the linear logic with least and greatest fixed-points. Indeed, while the proof theory of circular proofs made progress in the last twenty years, their denotational semantics is still underdeveloped. A denotational semantics for non-wellfounded proofs will be discussed in this talk. This semantics is used to investigate the denotational content of the standard translation from finitary proofs to non-wellfounded ones: it is shown that the translation from finitary proofs to circular ones is denotionally transparent. Moreover, we will talk about some properties of this semantics. The semantics is indeed sound in the sense that each proof of an infinite sequence of proofs converging by cut-elimination to a cut-free valid proof has the same interpretation as its limit. We will also see that valid proofs are interpreted as total elements of the semantics.