POPL 2023 (series) / POPL Research Papers /
Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework
We solve the inhabitation problem for a language called $\lambda$!, 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 $\lambda$!.
Fri 20 JanDisplayed time zone: Eastern Time (US & Canada) change
Fri 20 Jan
Displayed time zone: Eastern Time (US & Canada) change
09:00 - 10:15 | |||
09:00 25mTalk | A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F⋈ POPL Nick Rioux University of Pennsylvania, Xuejing Huang University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong, Steve Zdancewic University of Pennsylvania DOI | ||
09:25 25mTalk | Making a Type Difference: Subtraction on Intersection Types as Generalized Record Operations POPL Han Xu Peking University, Xuejing Huang University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong DOI | ||
09:50 25mTalk | Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework POPL Victor Arrial Université Paris Cité - CNRS - IRIF, Giulio Guerrieri Aix Marseille Université - CNRS - LIS; Edinburgh Research Centre - Central Software Institute - Huawei, Delia Kesner Université Paris Cité - CNRS - IRIF; Institut Universitaire de France DOI |