2024 Papers¶
Papers from 2024 across all venues.
POPL 2024¶
| Title | Authors | Topics |
|---|---|---|
| Soundly Handling Linearity | Tang, Hillerström, Lindley, Morris | linear types, algebraic effects, effect handlers |
| Modular Denotational Semantics for Effects with Guarded Interaction Trees | Frumin, Timany, Birkedal | denotational semantics, interaction trees, effects |
| Indexed Types for a Statically Safe WebAssembly | Geller, Frank, Bowman | WebAssembly, indexed types, static safety |
| The Essence of Generalized Algebraic Data Types | Sieczkowski, Stepanenko, Sterling, Birkedal | GADTs, type theory, category theory |
| Parametric Subtyping for Structural Parametric Polymorphism | DeYoung, Mordido, Pfenning, Das | subtyping, parametric polymorphism, session types |
| When Subtyping Constraints Liberate | Parreaux, Boruch-Gruszecki, Fan, Chau | type inference, first-class polymorphism |
| Polymorphic Type Inference for Dynamic Languages | Castagna, Laurent, Nguyễn | type inference, dynamic languages, semantic subtyping |
| Polynomial Time and Dependent Types | Atkey | dependent types, complexity, type theory |
| Internal Parametricity, without an Interval | Altenkirch, Chamoun, Kaposi, Shulman | parametricity, type theory, HoTT |
| Asynchronous Probabilistic Couplings in Higher-Order Separation Logic | Gregersen, Aguirre, Haselwarter, Tassarotti, Birkedal | separation logic, probabilistic programs |
| Nominal Recursors as Epi-Recursors | Popescu | nominal types, binding, recursion |
| Automatic Parallelism Management | Westrick, Fluet, Rainey, Acar | parallelism, functional programming |
| Deadlock-Free Separation Logic | Jacobs, Hinrichsen, Krebbers | separation logic, deadlock freedom, linear types |
| Flan: An Expressive and Efficient Datalog Compiler | Abeysinghe, Xhebraj, Rompf | Datalog, program analysis, compilation |
ICFP 2024¶
| Title | Authors | Topics |
|---|---|---|
| Error Credits: Resourceful Reasoning about Error Bounds | Aguirre, Haselwarter, de Medeiros, Li, Gregersen, Tassarotti, Birkedal | probabilistic programs, separation logic |
| Snapshottable Stores | Allain, Clément, Moine, Scherer | data structures, snapshots, OCaml |
| Example-Based Reasoning about the Realizability of Polymorphic Programs | Mulleners, Jeuring, Heeren | parametricity, polymorphism, testing |
| The Long Way to Deforestation | Chen, Parreaux | deforestation, type inference, optimization |
| Abstracting Effect Systems for Algebraic Effect Handlers | Yoshioka, Sekiyama, Igarashi | algebraic effects, abstract interpretation |
| Closure-Free Functional Programming in a Two-Level Type Theory | Kovács | two-level type theory, staging, closures |
| Gradual Indexed Inductive Types | Malewski Correa, Maillard, Tabareau, Tanter | gradual typing, dependent types |
| Almost-Sure Termination by Guarded Refinement | Gregersen, Aguirre, Haselwarter, Tassarotti, Birkedal | probabilistic termination, separation logic |
| Oxidizing OCaml with Modal Memory Management | Lorenzen, White, Dolan, Eisenberg, Lindley | OCaml, modal types, memory management |
| Sound Borrow-Checking for Rust via Symbolic Semantics | Ho, Fromherz, Protzenko | Rust, borrow checking, formal verification |
| A Coq Mechanization of JavaScript Regular Expression Semantics | De Santo, Barrière, Pit-Claudel | Coq, regular expressions, mechanization |
| CCLemma: E-Graph Guided Lemma Discovery | Kurashige, Ji, et al. | e-graphs, lemma discovery, inductive proofs |
PLDI 2024¶
| Title | Authors | Topics |
|---|---|---|
| RefinedRust: A Type System for High-Assurance Verification of Rust Programs | Gäher, Sammler, Jung, Krebbers, Dreyer | Rust, refinement types, verification |
| Verified Extraction from Coq to OCaml | Forster, Sozeau, Tabareau | Coq, extraction, formal verification |
| Stream Types | Cutler, Watson, et al. | stream types, corecursion, type systems |
| Space-Efficient Polymorphic Gradual Typing, Mostly Parametric | Igarashi, Ozaki, Sekiyama, Tanabe | gradual typing, polymorphism |
| Associated Effects | Lutze, Madsen | algebraic effects, type classes |
| Decidable Subtyping of Existential Types for Julia | Belyakova, Chung, Tate, Vitek | subtyping, existential types, Julia |
| Numerical Fuzz: A Type System for Rounding Error Analysis | Kellison, Hsu | floating-point, type systems, numerical analysis |
| Hyper Hoare Logic | Dardinier, Müller | Hoare logic, hyperproperties, security |
| Quest Complete: The Holy Grail of Gradual Security | Chen, Siek | gradual typing, security, information flow |
| Quiver: Guided Abductive Inference of Separation Logic Specifications | Spies, Gäher, Sammler, Dreyer | separation logic, specification inference, Coq |
| The Functional Essence of Imperative Binary Search Trees | Lorenzen, Leijen, Swierstra, Lindley | functional programming, in-place update |
| Bringing the WebAssembly Standard up to Speed with SpecTec | Youn, Wonho, et al. | WebAssembly, specification languages |
| Bit Blasting Probabilistic Programs | Garg, Holtzen, Van den Broeck, Millstein | probabilistic programming, exact inference |