Encoding Tight Typing in a Unified Framework
Delia Kesner, Andr\'es Viso

TL;DR
This paper introduces a unified, quantitative type system framework based on call-by-push-value that encodes and analyzes call-by-name and call-by-value, providing precise measures of normalization sequences.
Contribution
It proposes a unified tight type system in CBPV that encodes CBN and CBV, capturing exact normalization lengths and sizes, and distinguishes reduction types.
Findings
Quantitative type systems for CBN and CBV are encoded in CBPV.
Exact information about normalization sequence lengths and sizes is provided.
Reduction sequences are discriminated by multiplicative and exponential aspects.
Abstract
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 CBV that can be both encoded in a unique tight type system for CBPV. All such systems are quantitative, ie. they provide exact information about the length of normalization sequences to normal form as well as the size of these normal forms. Moreover, the length of reduction sequences are discriminated according to their multiplicative and exponential nature, a concept inherited from linear logic. Last but not least, it is possible to extract quantitative measures for CBN and CBV from their corresponding encodings in CBPV.
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.
