7 papers · 1 filter
Useful Evaluation: Syntax and Semantics (Technical Report)
Pablo Barenbaum, Delia Kesner, Mariana Milicich
This work provides the first inductive definition of useful CBV evaluation. For that, we first restrict the substitution operation in the Value Substitution Calculus to be linear,…
A Faithful and Quantitative Notion of Distant Reduction for the Lambda-Calculus with Generalized Applications
José EspÃrito Santo, Delia Kesner, Loïc Peyrot
We introduce a call-by-name lambda-calculus with generalized applications which is equipped with distant reduction. This allows to unblock -redexes without resorting to…
Hybrid Intersection Types for PCF (Extended Version)
Pablo Barenbaum, Delia Kesner, Mariana Milicich
Intersection type systems have been independently applied to different evaluation strategies, such as call-by-name (CBN) and call-by-value (CBV). These type systems have been then…
The Benefits of Diligence
Victor Arrial, Giulio Guerrieri, Delia Kesner
This paper studies the strength of embedding Call-by-Name ({\tt dCBN}) and Call-by-Value ({\tt dCBV}) into a unifying framework called the Bang Calculus ({\tt dBANG}). These embedd…
A Strong Bisimulation for a Classical Term Calculus
Eduardo Bonelli, Delia Kesner, Andrés Viso
When translating a term calculus into a graphical formalism many inessential details are abstracted away. In the case of -calculus translated to proof-nets, these inessential d…
Meaningfulness and Genericity in a Subsuming Framework
Delia Kesner, Victor Arrial, Giulio Guerrieri
This paper studies the notion of meaningfulness for a unifying framework called dBang-calculus, which subsumes both call-by-name (dCbN) and call-by-value (dCbV). We first character…