research
∙
09/21/2023
Strong Call-by-Value and Multi Types
This paper provides foundations for strong (that is, possibly under abst...
share
research
∙
03/14/2023
Normal Form Bisimulations By Value
Sangiorgi's normal form bisimilarity is call-by-name, identifies all the...
research
∙
01/29/2023
A Log-Sensitive Encoding of Turing Machines in the λ-Calculus
This note modifies the reference encoding of Turing machines in the λ-ca...
research
∙
07/18/2022
Multi Types and Reasonable Space (Long Version)
Accattoli, Dal Lago, and Vanoni have recently proved that the space used...
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
∙
05/30/2022
Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
This paper introduces the exponential substitution calculus (ESC), a new...
research
∙
03/01/2022
Reasonable Space for the λ-Calculus, Logarithmically
Can the λ-calculus be considered as a reasonable computational model? Ca...
research
∙
02/07/2022
Call-by-Value Solvability and Multi Types
This paper provides a characterization of call-by-value solvability usin...
research
∙
07/14/2021
Useful Open Call-by-Need
This paper studies useful sharing, which is a sophisticated optimization...
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/28/2021
The Space of Interaction (long version)
The space complexity of functional programs is not well understood. In p...
research
∙
02/13/2021
Strong Call-by-Value is Reasonable, Implosively
Whether the number of beta-steps in the lambda-calculus can be taken as ...
research
∙
10/24/2020
The (In)Efficiency of Interaction
Evaluating higher-order functional programs through abstract machines in...
research
∙
05/04/2020
Factorize Factorization
We present a new technique for proving factorization theorems for compou...
research
∙
02/19/2020
Functional Pearl: The Distributive λ-Calculus
We introduce a simple extension of the λ-calculus with pairs—called the ...
research
∙
02/13/2020
The Abstract Machinery of Interaction (Long Version)
This paper revisits the Interaction Abstract Machine (IAM), a machine ba...
research
∙
08/29/2019
Factorization and Normalization, Essentially
Lambda-calculi come with no fixed evaluation strategy. Different strateg...
research
∙
07/13/2019
Sharing Equality is Linear
The λ-calculus is a handy formalism to specify the evaluation of higher-...
research
∙
07/13/2019
Crumbling Abstract Machines
Extending the lambda-calculus with a construct for sharing, such as let ...
research
∙
02/15/2019
Types by Need (Extended Version)
A cornerstone of the theory of lambda-calculus is that intersection type...
research
∙
08/30/2018
Types of Fireballs (Extended Version)
The good properties of Plotkin's call-by-value lambda-calculus crucially...
research
∙
08/10/2018
Proof Nets and the Linear Substitution Calculus
Since the very beginning of the theory of linear logic it is known how t...
research
∙
07/06/2018
Tight Typings and Split Bounds
Multi types---aka non-idempotent intersection types---have been used to ...
research
∙
11/28/2017
The Maximal MAM, a Reasonable Implementation of the Maximal Strategy
This note is about a reasonable abstract machine, called Maximal MAM, im...
research
∙
11/28/2017