| 2-Functoriality of Initial Semantics |
Ahrens, Lafont, Lamiaux |
type theory, category theory |
| Almost Fair Simulations |
Correnson, Kuhn, Finkbeiner |
concurrency, semantics |
| Bialgebraic Reasoning on Stateful Languages |
— |
semantics, bialgebra |
| Big Steps in Higher-Order Mathematical Operational Semantics |
— |
operational semantics |
| Call-Guarded Abstract Definitional Interpreters |
— |
abstract interpretation |
| Compiling with Generating Functions |
— |
compilers |
| Correctness Meets Performance: From Agda to Futhark |
— |
verified compilation |
| CRDT Emulation, Simulation, and Representation Independence |
— |
distributed systems, CRDTs |
| Effectful Lenses: There and Back with Different Monads |
— |
lenses, monads |
| Environment-Sharing Analysis for Higher-Order Languages |
— |
compilers, analysis |
| First-Order Laziness |
Lorenzen, Leijen, Swierstra, Lindley |
functional programming, laziness |
| Formal Semantics and Program Logics for a Fragment of OCaml |
— |
formal verification, OCaml |
| Frex: Dependently Typed Algebraic Simplification |
Allais, Brady, Corbyn, Kammar, Yallop |
dependent types, proof assistants |
| Fusing Session-Typed Concurrent Programming into Functional Programming |
— |
session types, concurrency |
| Linear Types with Dynamic Multiplicities in Dependent Type Theory |
— |
linear types, dependent types |
| McTT: A Verified Kernel for a Proof Assistant |
Jang, Gaulin, Hu, Pientka |
proof assistants, dependent types |
| Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs |
— |
concurrency, probabilistic |
| Multi-stage Programming with Splice Variables |
Tsung-Ju Chiang, Ningning Xie |
multi-stage programming, type systems |
| Multiple Resumptions and Local Mutable State, Directly |
— |
algebraic effects |
| Normalization by Evaluation for Non-cumulativity |
Jiang, Hu, Oliveira |
dependent types, NbE |
| Reasoning about Weak Isolation Levels in Separation Logic |
— |
concurrency, separation logic |
| Relax! The Semilenient Core of Choreographic Programming |
— |
choreographic programming |
| Robust Dynamic Embedding for Gradual Typing |
Jacobs, Toro, Tabareau, Tanter |
gradual typing |
| SecRef*: Securely Sharing Mutable References |
Andrici, Ahman, Hriţcu, Icleanu |
formal verification, F*, security |
| Type Theory in Type Theory using a Strictified Syntax |
Kaposi, Pujet |
type theory, metatheory |
| Type Universes as Kripke Worlds |
Koronkevich, Bowman |
dependent types, universes |
| Verified Interpreters for Dynamic Languages — Nix |
— |
formal verification, dynamic languages |
| Verifying Graph Algorithms in Separation Logic |
— |
formal verification, graph algorithms |