Fri 20 Jan 2023 09:50 - 10:15 at Avenue34 - Types II Chair(s): Alan Jeffrey

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 Jan

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 10:15
Types IIPOPL at Avenue34
Chair(s): Alan Jeffrey Roblox
09:00
25m
Talk
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
25m
Talk
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
25m
Talk
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