Types by Need (Extended Version)
Beniamino Accattoli, Giulio Guerrieri, Maico Leberle

TL;DR
This paper introduces a novel multi type system for call-by-need evaluation in lambda calculus, providing exact bounds on evaluation lengths and establishing a precise denotational model for call-by-need, advancing the quantitative understanding of this evaluation strategy.
Contribution
It develops the first multi type system for call-by-need that yields exact evaluation bounds and offers a tight quantitative denotational semantics.
Findings
Provides exact bounds for call-by-need evaluation lengths
Induces a denotational model of call-by-need
Advances quantitative semantics of lambda calculus
Abstract
A cornerstone of the theory of lambda-calculus is that intersection types characterise termination properties. They are a flexible tool that can be adapted to various notions of termination, and that also induces adequate denotational models. Since the seminal work of de Carvalho in 2007, it is known that multi types (i.e. non-idempotent intersection types) refine intersection types with quantitative information and a strong connection to linear logic. Typically, type derivations provide bounds for evaluation lengths, and minimal type derivations provide exact bounds. De Carvalho studied call-by-name evaluation, and Kesner used his system to show the termination equivalence of call-by-need and call-by-name. De Carvalho's system, however, cannot provide exact bounds on call-by-need evaluation lengths. In this paper we develop a new multi type system for call-by-need. Our system…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Formal Methods in Verification
