research
∙
09/21/2023
Strong Call-by-Value and Multi Types
This paper provides foundations for strong (that is, possibly under abst...
share
research
∙
08/15/2023
Infinitary cut-elimination via finite approximations
We investigate non-wellfounded proof systems based on parsimonious logic...
research
∙
07/18/2022
The Theory of Call-by-Value Solvability (long version)
The denotational semantics of the untyped lambda-calculus is a well deve...
research
∙
04/19/2022
Strategies for Asymptotic Normalization
We present a technique to study normalizing strategies when termination ...
research
∙
02/07/2022
Call-by-Value Solvability and Multi Types
This paper provides a characterization of call-by-value solvability usin...
research
∙
12/30/2021
A Deep Inference System for Differential Linear Logic
Differential linear logic (DiLL) provides a fine analysis of resource co...
research
∙
04/28/2021
Semantic Bounds and Strong Call-by-Value Normalization
This paper explores two topics at once: the use of denotational semantic...
research
∙
04/20/2021
On reduction and normalization in the computational core
We study the reduction in a lambda-calculus derived from Moggi's computa...
research
∙
01/20/2021
Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic (long version)
In each variant of the lambda-calculus, factorization and normalization ...
research
∙
08/06/2020
Gluing resource proof-structures: inhabitation and inverting the Taylor expansion
A Multiplicative-Exponential Linear Logic (MELL) proof-structure can be ...
research
∙
05/04/2020
Factorize Factorization
We present a new technique for proving factorization theorems for compou...
research
∙
02/19/2020
Decomposing Probabilistic Lambda-calculi
A notion of probabilistic lambda-calculus usually comes with a prescribe...
research
∙
10/17/2019
Glueability of resource proof-structures: inverting the Taylor expansion (long version)
A Multiplicative-Exponential Linear Logic (MELL) proof-structure can be ...
research
∙
08/29/2019
Factorization and Normalization, Essentially
Lambda-calculi come with no fixed evaluation strategy. Different strateg...
research
∙
07/13/2019
Crumbling Abstract Machines
Extending the lambda-calculus with a construct for sharing, such as let ...
research
∙
04/23/2019
Towards a Semantic Measure of the Execution Time in Call-by-Value lambda-Calculus
We investigate the possibility of a semantic account of the execution ti...
research
∙
04/15/2019
The Bang Calculus and the Two Girard's Translations
We study the two Girard's translations of intuitionistic implication int...
research
∙
02/15/2019
Types by Need (Extended Version)
A cornerstone of the theory of lambda-calculus is that intersection type...
research
∙
12/27/2018
Towards a Semantic Measure of the Execution Time in Call-by-Value lambda-Calculus (Long Version)
We investigate the possibility of a semantic account of the execution ti...
research
∙
08/30/2018