## Presentation |
## Contact |
## Research |
## Teaching |
## CV |
## Other |

- J.Chouquet and C.Tasson (to be presented at CSL 2020, Barcelona)
:

Taylor expansion for Call-By-Push-Value

AbstractWe introduce a resource calculus for Call-By-Push-Value, and use it to define Taylor expansion. We show that it is consistent with Call-By-Push-Value operational and denotational semantics, using methods inspired from Linear Logic. Our work focuses in particular in giving a syntactical account to the coalgebras morphisms in the semantics.

- J. Chouquet (MFPS 2019) :

Taylor expansion, finiteness and strategies

AbstractWe examine some recent methods introduced to extend Ehrhard and Regnier's result on Taylor expansion: infinite linear combinations of approximants of a lambda-term can be normalized while keeping all coefficients finite. The methods considered allow to extend this result to non-uniform calculi; we show that when focusing on precise reduction strategies, such as Call-By-Value, Call-By-Need, PCF or variants of Call-By-Push-Value, the extension of Ehrhard and Regnier's finiteness result can hold or not, depending on the structure of the original calculus. In particular, we introduce a resource calculus for Call-By-Need, and show that the finiteness result about its Taylor expansion can be derived from our Call-By-Value considerations. We also introduce a resource calculus for a presentation of PCF with an explicit fixpoint construction, and show how it interferes with the finiteness result. We examine then Ehrhard and Guerrieri's Bang Calculus which enjoys some Call-By-Push-Value features in a slightly different presentation.

- J. Chouquet et L. Vaux-Auclair (CSL 2018) :

An application of parallel cut elimination in unit-free multiplicative linear logic to the Taylor expansion of proof nets

AbstractWe study parallel cut elimination in the connected, multiplicative fragment of linear logic proof nets, and provide a bound on the diminution of size, and on the length of switching paths under parallel reduction. We show that this combinatorial result applies to Taylor expansion of MELL proof nets, and allows to establish that coefficients keep finite under parallel reduction of infinite linear combination of resource nets, because they behave exactly like multiplicative nets.

- J. Chouquet et L. Vaux-Auclair :

An application of parallel cut elimination in multiplicative linear logic to the Taylor expansion of proof nets

AbstractWe extend the results of our CSL paper, generalizing it to a larger fragment of linear logic, including weakenings and multiplicative units. It demands specific methods to deal with non connected structures, in particular because of cuts reducing to empty substructures.

- Une géométrie du calcul (in french).
- Slides of the defense.

- Topological insights on probabilistic agreement Presentation of results on combinatorial topology applied to probabilistic distributed algorithms. Invitation at Verimag seminar, Grenoble, february 2020.
- Taylor expansion for Call-By-Push-Value Présentation of the CSL 2020 paper, written with Christine Tasson.
- Ma vie, mon œuvre Presentation at the «UFR d’informatique de l’Université de Paris». September, 2019.
- Cut-elimination in Taylor expansion of proof nets Presentation at the "journées PPS" 2018
- Paths and jumps in taylor expansion of proof nets Presentation at the workshop "Proof-nets" of the GDR Linear Logic, Villetaneuse, 2018

- Estonian winter school in computer science, Palmse, 2020
- Seminar Vérimag, Grenoble, 2020
- CSL, Barcelona, 2020
- MFPS, London, 2019
- Computer science department, Université de Paris, 2019
- Workshop on proof nets od GDRI Linear Logic, Villetaneuse, 2018
- CSL, Birmingham, 2018
- Seminar of team LdP, I2M, Marseilles, 2018
- "Journées PPS", 2018
- Meeting of GDRI Linear Logic, Roma, 2017
- ChoCola Meeting, Lyon, 2017
- Phd Seminar, Irif, Paris, 2017
- TLLA, Oxford, 2017