POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Fri 19 Jan 2024 11:30 - 11:50 at Turing Lecture - Type Theory Chair(s): Kuen-Bang Hou (Favonia)

We combine dependent types with linear type systems that soundly and completely capture polynomial time computation. We explore two systems for capturing polynomial time: one system that disallows construction of iterable data, and one, based on the LFPL system of Martin Hofmann, that controls construction via a payment method. Both of these are extended to full dependent types via Quantitative Type Theory, allowing for arbitrary computation in types alongside guaranteed polynomial time computation in terms. We prove the soundness of the systems using a realisability technique due to Dal Lago and Hofmann.

Our long-term goal is to combine the extensional reasoning of type theory with intensional reasoning about the resources intrinsically consumed by programs. This paper is a step along this path, which we hope will lead both to practical systems for reasoning about programs’ resource usage, and to theoretical use as a form of synthetic computational complexity theory.

Fri 19 Jan

Displayed time zone: London change

10:30 - 11:50
Type TheoryPOPL at Turing Lecture
Chair(s): Kuen-Bang Hou (Favonia) University of Minnesota
10:30
20m
Talk
Internal parametricity, without an interval
POPL
Thorsten Altenkirch University of Nottingham, Yorgo Chamoun École Polytechnique, Ambrus Kaposi Eötvös Loránd University, Michael Shulman University of San Diego
Pre-print
10:50
20m
Talk
Internal and Observational Parametricity for Cubical Agda
POPL
Antoine Van Muylder KU Leuven, Andreas Nuyts KU Leuven, Belgium, Dominique Devriese KU Leuven
11:10
20m
Talk
Internalizing Indistinguishability with Dependent TypesRemote
POPL
Yiyun Liu University of Pennsylvania, Jonathan Chan University of Pennsylvania, Jessica Shi University of Pennsylvania, Stephanie Weirich University of Pennsylvania
11:30
20m
Talk
Polynomial Time and Dependent types
POPL
Robert Atkey University of Strathclyde