Delia Kesner

Encoding Tight Typing in a Unified Framework

2021 · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics)

This paper explores how the intersection type theories of call-by-name (CBN) and call-by-value (CBV) can be unified in a more general framework provided by call-by-push-value (CBPV). Indeed, we propose tight type systems for CBN and …

Useful Call-by-Value: A Semantic Interpretation via Quantitative Types

2024 · arXiv (Cornell University)

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, yielding the LCBV strategy. We then further restrict …

The Benefits of Diligence

2024 · Lecture notes in computer science

Abstract This paper studies the strength of embedding Call-by-Name () and Call-by-Value () into a unifying framework called the Bang Calculus (). These embeddings enable establishing (static and dynamic) properties of and through their respective …