一句话：提出统一框架求解 λ! 的定量 inhabitation，并为可编码进 λ! 的多种 lambda 演算导出 inhabitation 算法。
论文研究 λ! 语言中的 inhabitation 问题。λ! 是受 call-by-push-value 启发的统一范式，可编码 call-by-name 与 call-by-value 等函数式求值策略。作者用非幂等交集类型系统给出类型规格，该系统能刻画程序动态行为的定量性质。通过统一方法，他们解决 λ! 的 inhabitation 问题，并展示如何为可编码进 λ! 的不同 lambda 演算推导相应的 inhabitation 算法。关键结果是该框架对多种演算的通用性，以及非幂等交集类型在定量 inhabitation 分析中的作用。
We solve the inhabitation problem for a language called λ!, a subsuming paradigm (inspired by call-by-push-value) being able to encode, among others, call-by-name and call-by-value strategies of functional programming. The type specification uses a non-idempotent intersection type system, which is able to capture quantitative properties about the dynamics of programs. As an application, we show how our general methodology can be used to derive inhabitation algorithms for different lambda-calculi that are encodable into λ!.
@article{paperbot2095,
title = {Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework},
author = {Victor Arrial and Giulio Guerrieri and Delia Kesner},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571244}
}