Split Decisions: Explicit Contexts for Substructural Languages
distinguished paper
This program is tentative and subject to change.
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 JanDisplayed time zone: Mountain Time (US & Canada) change
11:00 - 12:30 | |||
11:00 30mTalk | 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 30mTalk | Machine Checked Proofs and Programs in Algebraic Combinatorics CPP Florent Hivert Univ. Paris-Saclay, LISN, LMF, CNRS, INRIA | ||
12:00 30mTalk | 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 |