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

- 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 (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 :

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.

- J.Chouquet and C.Tasson :Taylor expansion for Call-By-Push-Value

- 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
- Taylor expansion, finiteness and strategies Presentation of my paper at MFPS 2019 , London, june, 7.

- TLLA, Oxford, 2017
- Meeting of GDRI Linear Logic, Roma, 2017
- ChoCola Meeting, Lyon, 2017
- Workshop on proof nets od GDRI Linear Logic, Villetaneuse, 2018
- CSL, Birmingham, 2018
- Seminar of team LdP, I2M, Marseilles, 2018
- "JournÃ©es PPS", 2018
- MFPS, London, 2019