POPL 2025
Sun 19 - Sat 25 January 2025 Denver, Colorado, United States

This program is tentative and subject to change.

Fri 24 Jan 2025 11:40 - 12:00 at Peek-A-Boo - Types 2

We present \emph{Generic Refinement Types}: a way to write modular higher-order specifications that abstract invariants over function contracts, while preserving automatic SMT-decidable verification. We show how generic refinements let us write a variety of modular higher-order specifications, including specifications for Rust’s traits which abstract over the concrete refinements that hold for different trait implementations. We formalize generic refinements in a core calculus and show how to synthesize the generic instantiations algorithmically at usage sites via a combination of syntactic unification and constraint solving. We give semantics to generic refinements via the intuition that they correspond to \emph{ghost parameters}, and we formalize this intuition via a type-preserving translation into the polymorphic contract calculus to establish the soundness of generic refinements. Finally, we evaluate generic refinements by implementing them in Flux and using it for two case studies. First, we show how generic refinements let us write modular specifications for Rust’s vector indexing API that lets us statically verify the bounds safety of a variety of vector-manipulating benchmarks from the literature. Second, we use generic refinements to refine Rust’s DIesel ORM library to track the semantics of the database queries issued by client applications, and hence, statically enforce data-dependent access-control policies in several database-backed web applications.

This program is tentative and subject to change.

Fri 24 Jan

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

10:40 - 12:00
Types 2POPL at Peek-A-Boo
10:40
20m
Paper
Affect: An Affine Type and Effect System
POPL
Orpheas van Rooij University of Edinburgh, Robbert Krebbers Radboud University Nijmegen
Link to publication
11:00
20m
Talk
A modal deconstruction of Löb induction
POPL
Daniel Gratzer Aarhus University
11:20
20m
Talk
QuickSub: Efficient Iso-Recursive Subtyping
POPL
Litao Zhou University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
11:40
20m
Talk
Generic Refinement Types
POPL