POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Thu 18 Jan 2024 11:10 - 11:30 at Kelvin Lecture - Types 2 Chair(s): Stefan K. Muller

We present a logically principled foundation for systematizing, in a way that works with any computational effect and evaluation order, SMT constraint generation seen in refinement type systems for functional programming languages. By carefully combining a focalized variant of call-by-push-value, bidirectional typing, and our novel technique of value-determined indexes, our system generates solvable SMT constraints without existential (unification) variables. We design a polarized subtyping relation allowing us to prove our logically focused typing algorithm is sound, complete, and decidable. We prove type soundness of our declarative system with respect to an elementary domain-theoretic denotational semantics. Type soundness implies, relatively simply, the total correctness and logical consistency of our system. The relative ease with which we obtain both algorithmic and semantic results ultimately stems from the proof-theoretic technique of focalization.

Thu 18 Jan

Displayed time zone: London change

10:50 - 12:10
Types 2POPL at Kelvin Lecture
Chair(s): Stefan K. Muller Illinois Institute of Technology
10:50
20m
Talk
Quotient Haskell: Lightweight Quotient Types for All
POPL
Brandon Hewer University of Nottingham, Graham Hutton University of Nottingham, UK
11:10
20m
Talk
Focusing on Refinement Typing (TOPLAS)Remote
POPL
Dimitrios Economou Queen's University, Canada, Neel Krishnaswami University of Cambridge, Jana Dunfield Queen's University, Kingston, Ontario
Link to publication
11:30
20m
Talk
Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic ProgramsRemote
POPL
Guannan Wei Purdue University, Oliver Bračevac Galois, Inc., Songlin Jia Purdue University, USA, Yuyan Bao Augusta University, Tiark Rompf Purdue University
11:50
20m
Talk
Capturing Types (TOPLAS)
POPL
Aleksander Boruch-Gruszecki EPFL, Martin Odersky EPFL, Edward Lee University of Waterloo, Ondřej Lhoták University of Waterloo, Jonathan Immanuel Brachthäuser University of Tübingen
DOI File Attached