Composable Transactional Objects: A Position Paper -- Application-Scale Secure Multiparty Computation -- An Array-Oriented Language with Static Rank Polymorphism -- Gradual Typing for Annotated Type Systems -- Staged Composition Synthesis -- Overlapping and Order-Independent Patterns: Definitional Equality for All -- Verified Compilation for Shared-Memory C -- Verifying an Open Compiler Using Multi-language Semantics -- Impredicative Concurrent Abstract Predicates -- Local Reasoning for the POSIX File System -- A Coq Formalization of the Relational Data Model -- On Probabilistic Applicative Bisimulation and Call-by-Value λ-Calculi -- Grounding Synchronous Deterministic Concurrency in Sequential Programming -- The Duality of Construction -- Deriving Pretty-Big-Step Semantics from Small-Step Semantics -- Communicating State Transition Systems for Fine-Grained Concurrent Resources -- Checking Linearizability of Encapsulated Extended Operations -- Bounded Linear Types in a Resource Semiring -- A Core Quantitative Coeffect Calculus -- Measurements in Proof Nets as Higher-Order Quantum Circuits -- Automatic Termination Verification for Higher-Order Functional Programs -- An Abstract Domain to Infer Ordinal-Valued Ranking Functions -- Model and Proof Generation for Heap-Manipulating Programs -- REAP: Reporting Errors Using Alternative Paths -- The Network as a Language Construct -- Resolving Non-determinism in Choreographies -- A Correspondence between Two Approaches to Interprocedural Analysis in the Presence of Join -- Targeted Update – Aggressive Memory Abstraction Beyond Common Sense and Its Application on Static Numeric Analysis -- Affine Parallelization of Loops with Run-Time Dependent Bounds from Binaries.