PPaperPicks
← All conferences
Editions202620252024

POPL 2026

A*

ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Official site ↗
92
accepted papers
302
authors
January 11-17, 2026
dates
France
location

92 / 92 papers

  1. 1
    A Complementary Approach to Incorrectness Typing
    Celia Mengyue Li
    ,
    Sophie Pull
    ,
    Steven Ramsay
  2. 2
    A Family of Sims with Diverging Interests
    Nicolas Chappe
  3. 3
    A Lazy, Concurrent Convertibility Checker
    Nathanaëlle Courant
    ,
    Xavier Leroy
  4. 4
    A Logic for the Imprecision of Abstract Interpretations
    Marco Campion
    ,
    Mila Dalla Preda
    ,
    Roberto Giacobazzi
    ,
    Caterina Urban
  5. 5
    A Modular Static Cost Analysis for GPU Warp-Level Parallelism
    Gregory Blike
    ,
    Hannah Zicarelli
    ,
    Udaya Sathiyamoorthy
    ,
    Julien Lange
    ,
    Tiago Cogumbreiro
  6. 6
    A Relational Separation Logic for Effect Handlers
    Paulo Emílio de Vilhena
    ,
    Simcha van Collem
    ,
    Ines Wright
    ,
    Robbert Krebbers
  7. 7
    A Synthetic Reconstruction of Multiparty Session Types
    David Castro-Perez
    ,
    Francisco Ferreira
    ,
    Sung-Shik Jongmans
  8. 8
    A Verified High-Performance Composable Object Library for Remote Direct Memory Access
    Guillaume Ambal
    ,
    George Hodgkins
    ,
    Mark Madler
    ,
    Gregory V. Chockler
    ,
    Brijesh Dongol
    ,
    Joseph Izraelevitz
    ,
    Azalea Raad
    ,
    Viktor Vafeiadis
  9. 9
    Abstraction Functions as Types: Modular Verification of Cost and Behavior in Dependent Type Theory
    Harrison Grodin
    ,
    Runming Li
    ,
    Robert Harper
  10. 10
    Accelerating Syntax-Guided Program Synthesis by Optimizing Domain-Specific Languages
    Zhentao Ye
    ,
    Ruyi Ji
    ,
    Yingfei Xiong
    ,
    Xin Zhang
  11. 11
    AdapTT: Functoriality for Dependent Type Casts
    Arthur Adjedj
    ,
    Meven Lennon-Bertrand
    ,
    Thibaut Benjamin
    ,
    Kenji Maillard
  12. 12
    Algorithmic Conversion with Surjective Pairing: A Syntactic and Untyped Approach
    Yiyun Liu
    ,
    Stephanie Weirich
  13. 13
    All for One and One for All: Program Logics for Exploiting Internal Determinism in Parallel Programs
    Alexandre Moine
    ,
    Sam Westrick
    ,
    Joseph Tassarotti
  14. 14
    An Equational Axiomatization of Dynamic Threads via Algebraic Effects: Presheaves on Finite Relations, Labelled Posets, and Parameterized Algebraic Theories
    Ohad Kammar
    ,
    Jack Liell-Cock
    ,
    Sam Lindley
    ,
    Cristina Matache
    ,
    Sam Staton
  15. 15
    An Expressive Assertion Language for Quantum Programs
    Bonan Su
    ,
    Yuan Feng
    ,
    Mingsheng Ying
    ,
    Li Zhou
  16. 16
    Arbitration-Free Consistency Is Available (and Vice Versa)
    Hagit Attiya
    ,
    Constantin Enea
    ,
    Enrique Román-Calvo
  17. 17
    ArchSem: Reusable Rigorous Semantics of Relaxed Architectures
    Thibaut Pérami
    ,
    Thomas Bauereiss
    ,
    Brian Campbell
    ,
    Zongyuan Liu
    ,
    Nils Lauermann
    ,
    Alasdair Armstrong
    ,
    Peter Sewell
  18. 18
    Bayesian Separation Logic: A Logical Foundation and Axiomatic Semantics for Probabilistic Programming
    Shing Hin Ho
    ,
    Nicolas Wu
    ,
    Azalea Raad
  19. 19
    Big-Stop Semantics: Small-Step Semantics in a Big-Step Judgment
    David M. Kahn
    ,
    Jan Hoffmann
    ,
    Runming Li
  20. 20
    Bounded Sort Polymorphism with Elimination Constraints
    Johann Rosain
    ,
    Tomás Díaz
    ,
    Kenji Maillard
    ,
    Matthieu Sozeau
    ,
    Nicolas Tabareau
    ,
    Éric Tanter
    ,
    Théo Winterhalter
  21. 21
    Bounded Treewidth, Multiple Context-Free Grammars, and Downward Closures
    C. Aiswarya
    ,
    Pascal Baumann
    ,
    Prakash Saivasan
    ,
    Lia Schütze
    ,
    Georg Zetzsche
  22. 22
    Canonicity for Indexed Inductive-Recursive Types
    András Kovács
  23. 23
    Characterizing Sets of Theories That Can Be Disjointly Combined
    Benjamin Przybocki
    ,
    Guilherme Vicentin de Toledo
    ,
    Yoni Zohar
  24. 24
    ChiSA: Static Analysis for Lightweight Chisel Verification
    Jiacai Cui
    ,
    Qinlin Chen
    ,
    Zhongsheng Zhan
    ,
    Tian Tan
    ,
    Yue Li
  25. 25
    ChopChop: A Programmable Framework for Semantically Constraining the Output of Language Models
    Shaan Nagy
    ,
    Timothy Zhou
    ,
    Nadia Polikarpova
    ,
    Loris D'Antoni
  26. 26
    Classical Notions of Computation and the Hasegawa-Thielecke Theorem
    Éléonore Mangel
    ,
    Paul-André Melliès
    ,
    Guillaume Munch-Maccagnoni
  27. 27
    Coco: Corecursion with Compositional Heterogeneous Productivity
    Jaewoo Kim
    ,
    Yeonwoo Nam
    ,
    Chung-Kil Hur
  28. 28
    Compiling to Linear Neurons
    Joey Velez-Ginorio
    ,
    Nada Amin
    ,
    Konrad P. Kording
    ,
    Steve Zdancewic
  29. 29
    Consistent Updates for Scalable Microservices
    Devora Chait-Roth
    ,
    Kedar S. Namjoshi
    ,
    Thomas Wies
  30. 30
    Context-Free-Language Reachability for Almost-Commuting Transition Systems
    Nikhil Pimpalkhare
    ,
    Zachary Kincaid
    ,
    Thomas Reps
  31. 31
    Corrigendum: Unrealizability Logic
    Jinwoo Kim
    ,
    Loris D'Antoni
    ,
    Thomas Reps
  32. 32
    Counting and Sampling Traces in Regular Languages
    Alexis de Colnet
    ,
    Kuldeep S. Meel
    ,
    Umang Mathur
  33. 33
    Cryptis: Cryptographic Reasoning in Separation Logic
    Arthur Azevedo de Amorim
    ,
    Amal Ahmed
    ,
    Marco Gaboardi
  34. 34
    DafnyMPI: A Dafny Library for Verifying Message-Passing Concurrent Programs
    Aleksandr Fedchin
    ,
    Antero Mejr
    ,
    Hari Sundar
    ,
    Jeffrey S. Foster
  35. 35
    Dependent Coeffects for Local Sensitivity Analysis
    Victor Sannier
    ,
    Patrick Baillot
  36. 36
    Determination Problems for Orbit Closures and Matrix Groups
    Rida Ait El Manssour
    ,
    George Kenison
    ,
    Mahsa Shirmohammadi
    ,
    Anton Varonka
    ,
    James Worrell
  37. 37
    Di- is for Directed: First-Order Directed Type Theory via Dinaturality
    Andrea Laretto
    ,
    Fosco Loregiàn
    ,
    Niccolò Veltri
  38. 38
    Domain-Theoretic Semantics for Functional Logic Programming
    Eddie Jones
    ,
    Samson Main
    ,
    Celia Mengyue Li
    ,
    Jonathan Marriott
    ,
    G. A. Kavvos
  39. 39
    Encode the Cake and Eat It Too: Controlling Computation in Type Theory, Locally
    Yann Leray
    ,
    Théo Winterhalter
  40. 40
    Endangered by the Language But Saved by the Compiler: Robust Safety via Semantic Back-Translation
    Niklas Mück
    ,
    Aïna Linn Georges
    ,
    Derek Dreyer
    ,
    Deepak Garg
    ,
    Michael Sammler
  41. 41
    Extensible Data Types with Ad-Hoc Polymorphism
    Matthew Toohey
    ,
    Yanning Chen
    ,
    Ara Jamalzadeh
    ,
    Ningning Xie
  42. 42
    Formal Verification for JavaScript Regular Expressions: A Proven Mechanized Semantics and Its Applications
    Aurèle Barrière
    ,
    Victor Deng
    ,
    Clément Pit-Claudel
  43. 43
    Foundational Multi-Modal Program Verifiers
    Vladimir Gladshtein
    ,
    George Pîrlea
    ,
    Qiyuan Zhao
    ,
    Vitaly Kurin
    ,
    Ilya Sergey
  44. 44
    From Semantics to Syntax: A Type Theory for Comprehension Categories
    Niyousha Najmaei
    ,
    Niels van der Weide
    ,
    Benedikt Ahrens
    ,
    Paige Randall North
  45. 45
    Fuzzing Guided by Bayesian Program Analysis
    Yifan Zhang
    ,
    Xin Zhang
  46. 46
    General Decidability Results for Systems with Continuous Counters
    A. R. Balasubramanian
    ,
    Matthew Hague
    ,
    Rupak Majumdar
    ,
    Ramanathan S. Thinniyam
    ,
    Georg Zetzsche
  47. 47
    Generating Compilers for Qubit Mapping and Routing
    Abtin Molavi
    ,
    Amanda Xu
    ,
    Ethan Cecchetti
    ,
    Swamit Tannu
    ,
    Aws Albarghouthi
  48. 48
    Hadamard-Pi: Equational Quantum Programming
    Wang Fang
    ,
    Chris Heunen
    ,
    Robin Kaarsgaard
  49. 49
    Handling Higher-Order Effectful Operations with Judgemental Monadic Laws
    Zhixuan Yang
    ,
    Nicolas Wu
  50. 50
    Handling Scope Checks: A Comparative Framework for Dynamic Scope Extrusion Checks
    Michael Lee
    ,
    Ningning Xie
    ,
    Oleg Kiselyov
    ,
    Jeremy Yallop