POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France
Thu 15 Jan 2026 16:35 - 17:00 at Réfectoire - Security and Privacy Chair(s): Stephanie Weirich

Substructural type systems provide the ability to speak about resources. By enforcing usage restrictions on inputs to computations they allow programmers to reify limited system units—such as memory—in types. We demonstrate a new form of resource reasoning founded on constraining outputs and explore its utility for practical programming. In particular, we identify a number of disparate programming features explored largely in the security literature as various fragments of our unified framework. These encompass capabilities, quantitative information leakage, sandboxing in the style of the Linux seccomp interface, authorization protocols, and more. We furthermore explore its connection to conventional input-based resource reasoning, casting it as an internal treatment of the constructive Kripke semantics of substructural logics. We verify the capability, quantity, and protocol safety of our system through a single logical relations argument. In doing so, we take the first steps towards obtaining the ultimate multitool for security reasoning.

Thu 15 Jan

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

16:10 - 17:00
Security and PrivacyPOPL at Réfectoire
Chair(s): Stephanie Weirich University of Pennsylvania
16:10
25m
Talk
Dependent Coeffects for Local Sensitivity Analysis
POPL
Victor Sannier Univ. Lille - CNRS - Inria - Centrale Lille - UMR 9189 CRIStAL, Patrick Baillot Univ. Lille - CNRS - Inria - Centrale Lille - UMR 9189 CRIStAL
DOI
16:35
25m
Talk
Security Reasoning via Substructural Dependency TrackingDistinguished Paper
POPL
Hemant Gouni Carnegie Mellon University, Frank Pfenning Carnegie Mellon University, USA, Jonathan Aldrich Carnegie Mellon University
DOI Pre-print