Loïc Peyrot

PhD student at IRIF (université Paris Cité) under the supervision of Delia Kesner. I will be defending on the 18th of November! You can find the current version of the thesis here.

In my PhD, I work on two computational models: node replication and generalized applications, within the abstract setting of the λ-calculus.

These extensions have their origin in computational interpretations of proof theory. My coauthors and I develop operational semantics for them, in order to give more concrete implementations of computation, oriented from the perspective of programming languages.

Our approach also is guided by non-idempotent intersection type systems. Those systems can type exactly all terminating programs. We thus obtain a simple model of termination. Adding non-idempotence achieves a quantitative analysis of programs, giving for instance bounds on the length of computation and on the size of the results.

Published articles

Solvability for Generalized Applications, with Delia Kesner (FSCD ’22).

DOI: 10.4230/LIPIcs.FSCD.2022.18Slides

Abstract: Solvability is a key notion in the theory of call-by-name λ-calculus, used in particular to identify meaningful terms. However, adapting this notion to other call-by-name calculi, or extending it to different models of computation – such as call-by-value –, is not straightforward. In this paper, we study solvability for call-by-name and call-by-value λ-calculi with generalized applications, both variants inspired from von Plato’s natural deduction with generalized elimination rules. We develop an operational as well as a logical theory of solvability for each of them. The operational characterization relies on a notion of solvable reduction for generalized applications, and the logical characterization is given in terms of typability in an appropriate non-idempotent intersection type system. Finally, we show that solvability in generalized applications and solvability in the λ-calculus are equivalent notions.

A Faithful and Quantitative Notion of Distant Reduction for Generalized Applications, with José Espírito Santo and Delia Kesner (FoSSaCS ’22).

DOI: 10.1007/978-3-030-99253-8_15Slides

Abstract: We introduce a call-by-name lambda-calculus λJ with generalized applications which integrates a notion of distant reduction that allows to unblock β-redexes without resorting to the permutative conversions of generalized applications. We show strong normalization of simply typed terms, and we then fully characterize strong normalization by means of a quantitative typing system. This characterization uses a non-trivial inductive definition of strong normalization –that we relate to others in the literature–, which is based on a weak-head normalizing strategy. Our calculus relates to explicit substitution calculi by means of a translation between the two formalisms which is faithful, in the sense that it preserves strong normalization. We show that our calculus λJ and the well-know calculus ΛJ determine equivalent notions of strong normalization. As a consequence, ΛJ inherits a faithful translation into explicit substitutions, and its strong normalization can be characterized by the quantitative typing system designed for λJ, despite the fact that quantitative subject reduction fails for permutative conversions.

The Spirit of Node Replication, with Delia Kesner and Daniel Ventura (FoSSaCS ’21).

DOI: 10.1007/978-3-030-71995-1_18Slides

Abstract: We define and investigate a term calculus implementing higher-order node replication. We use the new calculus to specify two different (weak) evaluation strategies: call-by-name and fully lazy call-by-need. We show that they are observationally equivalent using type theoretical technical tools.

Other talks

Past internships/jobs

Teaching

Contact

E-mail address: firstname DOT lastname AT irif DOT fr

Physical address:

IRIF, office 3010
Bâtiment Sophie Germain
Université Paris Cité, campus Paris Rive Gauche
75013 Paris