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

This program is tentative and subject to change.

Mon 20 Jan 2025 11:00 - 11:30 at Marco Polo - Session 2 Chair(s): Jennifer Paykin

A central challenge in mechanizing the meta-theory of substructural languages is modeling contexts. Although various ad hoc approaches to this problem exist, we lack a set of good practices and a general infrastructure that can be leveraged for mechanizing a wide range of substructural systems.

In this work, we describe Contexts as Resource Vectors (CARVe), a general syntactic infrastructure for managing substructural contexts, where elements are annotated with tags from a resource algebra denoting their availability. Assumptions persist as contexts are manipulated since we model resource consumption by changing their tags. We may thus define relations between substructural contexts via simultaneous substitutions without the need to split them. Moreover, we establish a series of algebraic and well-formedness properties about context operations that are typically required to carry out proofs in practice. CARVe is implemented in the proof assistant Beluga.

To illustrate best practices for using our infrastructure, we give a detailed reformulation of the linear sequent calculus and bidirectional linear λ-calculus in terms of CARVe’s context operations and prove their equivalence using the aforementioned algebraic properties. In addition, we apply CARVe to mechanize a diverse set of systems, from the affine λ-calculus to the session-typed process calculus CP, giving us confidence that CARVe is sufficiently general to mechanize a broad range of substructural systems.

This program is tentative and subject to change.

Mon 20 Jan

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

11:00 - 12:30
Session 2CPP at Marco Polo
Chair(s): Jennifer Paykin Intel
11:00
30m
Talk
Split Decisions: Explicit Contexts for Substructural Languagesdistinguished paper
CPP
Daniel Zackon McGill University, Chuta Sano McGill University, Alberto Momigliano Università degli Studi di Milano, Brigitte Pientka McGill University
11:30
30m
Talk
Machine Checked Proofs and Programs in Algebraic Combinatorics
CPP
Florent Hivert Univ. Paris-Saclay, LISN, LMF, CNRS, INRIA
12:00
30m
Talk
Monadic interpreters for concurrent memory models: Executable semantics of a concurrent subset of LLVM IRremote presentation
CPP
Nicolas Chappe Inria Lyon, LIP, Ludovic Henrio University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP, Yannick Zakowski Inria
Hide past events
:
:
:
: