Presentation |
Contact |
Research |
Teaching |
CV |
Other |
We 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.
We 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.
We 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.
We 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.