2026 Papers¶
Papers from 2026 across all venues.
POPL 2026¶
| Title | Authors | Topics |
|---|---|---|
| Local Contextual Type Inference | Xu Xue, Chen Cui, Shengyi Jiang, Bruno C. d. S. Oliveira | type inference, bidirectional typing |
| Extensible Data Types with Ad-Hoc Polymorphism | Matthew Toohey, Yanning Chen, Ara Jamalzadeh, Ningning Xie | type systems, extensible types |
| Let Generalization, Polymorphic Recursion, and Variable Minimization in Boolean-Kinded Type Systems | Joseph Zullo | type inference, boolean types |
| Typing Strictness | Daniel Sainati, Joseph W. Cutler, Benjamin C. Pierce, Stephanie Weirich | type systems, laziness |
| Lazy Linearity for a Core Functional Language | Rodrigo Mesquita, Bernardo Toninho | linear types, functional programming |
| Miri: Practical Undefined Behavior Detection for Rust | Ralf Jung et al. | formal verification, Rust |
| Formal Verification for JavaScript Regular Expressions | Aurèle Barrière, Victor Deng, Clément Pit-Claudel | formal verification, mechanized semantics |
| TypeDis: A Type System for Disentanglement | Alexandre Moine, Stephanie Balzer, Alex Xu, Sam Westrick | type systems, parallelism, memory management |
| All for One and One for All: Program Logics for Internal Determinism | Alexandre Moine, Sam Westrick, Joseph Tassarotti | program logics, parallelism, separation logic |
| An Equational Axiomatization of Dynamic Threads via Algebraic Effects | Ohad Kammar, Jack Liell-Cock, Sam Lindley, Cristina Matache, Sam Staton | algebraic effects, concurrency, equational theory |
| The Relative Monadic Metalanguage | Jack Liell-Cock, Zev Shirazi, Sam Staton | relative monads, graded monads, denotational semantics |
| Counting and Sampling Traces in Regular Languages | Alexis de Colnet, Kuldeep S. Meel, Umang Mathur | regular languages, Mazurkiewicz traces, counting |
| Optimal Program Synthesis via Abstract Interpretation | Stephen Mell, Steve Zdancewic, Osbert Bastani | program synthesis, abstract interpretation, optimization |
| Hadamard-Pi: Equational Quantum Programming | Wang Fang, Chris Heunen, Robin Kaarsgaard | quantum programming, equational theory, reversible computing |
| Arbitration-Free Consistency Is Available (and Vice Versa) | Hagit Attiya, Constantin Enea, Enrique Román-Calvo | distributed systems, consistency models, availability |
| Oriented Metrics for Bottom-Up Enumerative Synthesis | Ria Ramesh, Thomas Bourgeat, Adam Chlipala | program synthesis, enumerative synthesis, search guidance |
| Compiling to Linear Neurons | Joey Velez-Ginorio, Sriram Sankaranarayanan, Swarat Chaudhuri | neural networks, compilation, program semantics |
| ChiSA: Static Analysis for Lightweight Chisel Verification | Jiacai Cui, Qinlin Chen, Zhongsheng Zhan, Tian Tan, Yue Li | hardware verification, static analysis, Chisel |
| Parameterized Verification of Quantum Circuits | Parosh Aziz Abdulla et al. | quantum circuits, parameterized verification, automata theory |
| Recurrence Sets for Proving Fair Non-termination under Axiomatic Memory Consistency Models | Thomas Haas, Roland Meyer, Hernán Ponce de León, Andrés Lomelí Garduño | non-termination, concurrency, weak memory models |
| Network Change Validation with Relational NetKAT | Han Xu, Zachary Kincaid, Ratul Mahajan, David Walker | network verification, NetKAT, relational semantics |