PPaperPicks
← All conferences
Editions202620252024

POPL 2025

A*

ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Official site ↗
79
accepted papers
272
authors
January 19-25, 2025
dates
United States
location

79 / 79 papers

  1. 1
    A Demonic Outcome Logic for Randomized Nondeterminism
    Noam Zilberstein
    ,
    Dexter Kozen
    ,
    Alexandra Silva
    ,
    Joseph Tassarotti
  2. 2
    A Dependent Type Theory for Meta-programming with Intensional Analysis
    Jason Z. S. Hu
    ,
    Brigitte Pientka
  3. 3
    A Modal Deconstruction of Löb Induction
    Daniel Gratzer
  4. 4
    A Primal-Dual Perspective on Program Verification Algorithms
    Takeshi Tsukada
    ,
    Hiroshi Unno
    ,
    Oded Padon
    ,
    Sharon Shoham
  5. 5
    A Quantitative Probabilistic Relational Hoare Logic
    Martin Avanzini
    ,
    Gilles Barthe
    ,
    Davide Davoli
    ,
    Benjamin Grégoire
  6. 6
    A Taxonomy of Hoare-Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests
    Lena Verscht
    ,
    Benjamin Lucien Kaminski
  7. 7
    A Verified Foreign Function Interface between Coq and C
    Joomy Korkut
    ,
    Kathrin Stark
    ,
    Andrew W. Appel
  8. 8
    Abstract Operational Methods for Call-by-Push-Value
    Sergey Goncharov
    ,
    Stelios Tsampas
    ,
    Henning Urbat
  9. 9
    Affect: An Affine Type and Effect System
    Orpheas van Rooij
    ,
    Robbert Krebbers
  10. 10
    Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order Programs
    Taro Sekiyama
    ,
    Hiroshi Unno
  11. 11
    Algebras for Deterministic Computation Are Inherently Incomplete
    Balder ten Cate
    ,
    Tobias Kappé
  12. 12
    All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants
    Josselin Poiret
    ,
    Gaëtan Gilbert
    ,
    Kenji Maillard
    ,
    Pierre-Marie Pédrot
    ,
    Matthieu Sozeau
    ,
    Nicolas Tabareau
    ,
    Éric Tanter
  13. 13
    An Incremental Algorithm for Algebraic Program Analysis
    Chenyu Zhou
    ,
    Yuzhou Fang
    ,
    Jingbo Wang
    ,
    Chao Wang
  14. 14
    Approximate Relational Reasoning for Higher-Order Probabilistic Programs
    Philipp G. Haselwarter
    ,
    Kwing Hei Li
    ,
    Alejandro Aguirre
    ,
    Simon Oddershede Gregersen
    ,
    Joseph Tassarotti
    ,
    Lars Birkedal
  15. 15
    Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer Casting
    Yonghyun Kim
    ,
    Minki Cho
    ,
    Jaehyung Lee
    ,
    Jinwoo Kim
    ,
    Taeyoung Yoon
    ,
    Youngju Song
    ,
    Chung-Kil Hur
  16. 16
    Automated Program Refinement: Guide and Verify Code Large Language Model with Refinement Calculus
    Yufan Cai
    ,
    Zhe Hou
    ,
    David Sanán
    ,
    Xiaokun Luan
    ,
    Yun Lin
    ,
    Jun Sun
    ,
    Jin Song Dong
  17. 17
    Automating Equational Proofs in Dirac Notation
    Yingte Xu
    ,
    Gilles Barthe
    ,
    Li Zhou
  18. 18
    Avoiding Signature Avoidance in ML Modules with Zippers
    Clement Blaudeau
    ,
    Didier Rémy
    ,
    Gabriel Radanne
  19. 19
    Axe 'Em: Eliminating Spurious States with Induction Axioms
    Neta Elad
    ,
    Sharon Shoham
  20. 20
    Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings
    Jan van Brügge
    ,
    James McKinna
    ,
    Andrei Popescu
    ,
    Dmitriy Traytel
  21. 21
    Bidirectional Higher-Rank Polymorphism with Intersection and Union Types
    Shengyi Jiang
    ,
    Chen Cui
    ,
    Bruno C. d. S. Oliveira
  22. 22
    Biparsers: Exact Printing for Data Synchronisation
    Ruifeng Xie
    ,
    Tom Schrijvers
    ,
    Zhenjiang Hu
  23. 23
    BiSikkel: A Multimode Logical Framework in Agda
    Joris Ceulemans
    ,
    Andreas Nuyts
    ,
    Dominique Devriese
  24. 24
    Bluebell: An Alliance of Relational Lifting and Independence for Probabilistic Reasoning
    Jialu Bao
    ,
    Emanuele D'Osualdo
    ,
    Azadeh Farzan
  25. 25
    Calculational Design of Hyperlogics by Abstract Interpretation
    Patrick Cousot
    ,
    Jeffery Wang
  26. 26
    CF-GKAT: Efficient Validation of Control-Flow Transformations
    Cheng Zhang
    ,
    Tobias Kappé
    ,
    David E. Narváez
    ,
    Nico Naus
  27. 27
    Coinductive Proofs for Temporal Hyperliveness
    Arthur Correnson
    ,
    Bernd Finkbeiner
  28. 28
    Compositional Imprecise Probability: A Solution from Graded Monads and Markov Categories
    Jack Liell-Cock
    ,
    Sam Staton
  29. 29
    Consistency of a Dependent Calculus of Indistinguishability
    Yiyun Liu
    ,
    Jonathan Chan
    ,
    Stephanie Weirich
  30. 30
    Data Race Freedom à la Mode
    Aïna Linn Georges
    ,
    Benjamin Peters
    ,
    Laila Elbeheiry
    ,
    Leo White
    ,
    Stephen Dolan
    ,
    Richard A. Eisenberg
    ,
    Chris Casinghino
    ,
    François Pottier
    ,
    Derek Dreyer
  31. 31
    Denotational Semantics of Gradual Typing using Synthetic Guarded Domain Theory
    Eric Giovannini
    ,
    Tingting Ding
    ,
    Max S. New
  32. 32
    Derivative-Guided Symbolic Execution
    Yongwei Yuan
    ,
    Zhe Zhou
    ,
    Julia Belyakova
    ,
    Suresh Jagannathan
  33. 33
    Dis/Equality Graphs
    George Zakhour
    ,
    Pascal Weisenburger
    ,
    Jahrim Gabriele Cesario
    ,
    Guido Salvaneschi
  34. 34
    Do You Even Lift? Strengthening Compiler Security Guarantees against Spectre Attacks
    Xaver Fabian
    ,
    Marco Patrignani
    ,
    Marco Guarnieri
    ,
    Michael Backes
  35. 35
    Finite-Choice Logic Programming
    Chris Martens
    ,
    Robert J. Simmons
    ,
    Michael Arntzenius
  36. 36
    Flexible Type-Based Resource Estimation in Quantum Circuit Description Languages
    Andrea Colledan
    ,
    Ugo Dal Lago
  37. 37
    Flo: A Semantic Foundation for Progressive Stream Processing
    Shadaj Laddad
    ,
    Alvin Cheung
    ,
    Joseph M. Hellerstein
    ,
    Mae Milano
  38. 38
    Formal Foundations for Translational Separation Logic Verifiers
    Thibault Dardinier
    ,
    Michael Sammler
    ,
    Gaurav Parthasarathy
    ,
    Alexander J. Summers
    ,
    Peter Müller
  39. 39
    Formalising Graph Algorithms with Coinduction
    Donnacha Oisín Kidney
    ,
    Nicolas Wu
  40. 40
    Fulminate: Testing CN Separation-Logic Specifications in C
    Rini Banerjee
    ,
    Kayvan Memarian
    ,
    Dhruv C. Makwana
    ,
    Christopher Pulte
    ,
    Neel Krishnaswami
    ,
    Peter Sewell
  41. 41
    Generic Refinement Types
    Nico Lehmann
    ,
    Cole Kurashige
    ,
    Nikhil Akiti
    ,
    Niroop Krishnakumar
    ,
    Ranjit Jhala
  42. 42
    Generically Automating Separation Logic by Functors, Homomorphisms, and Modules
    Qiyuan Xu
    ,
    David Sanán
    ,
    Zhe Hou
    ,
    Xiaokun Luan
    ,
    Conrad Watt
    ,
    Yang Liu
  43. 43
    Grove: A Bidirectionally Typed Collaborative Structure Editor Calculus
    Michael D. Adams
    ,
    Eric Griffis
    ,
    Thomas Porter
    ,
    Sundara Vishnu Satish
    ,
    Eric Zhao
    ,
    Cyrus Omar
  44. 44
    Guaranteed Bounds on Posterior Distributions of Discrete Probabilistic Programs with Loops
    Fabian Zaiser
    ,
    Andrzej S. Murawski
    ,
    C.-H. Luke Ong
  45. 45
    Inference Plans for Hybrid Particle Filtering
    Ellie Y. Cheng
    ,
    Eric Atkinson
    ,
    Guillaume Baudart
    ,
    Louis Mandel
    ,
    Michael Carbin
  46. 46
    Interaction Equivalence
    Beniamino Accattoli
    ,
    Adrienne Lancelot
    ,
    Giulio Manzonetto
    ,
    Gabriele Vanoni
  47. 47
    Linear and Non-linear Relational Analyses for Quantum Program Optimization
    Matthew Amy
    ,
    Joseph Lunderville
  48. 48
    Maximal Simplification of Polyhedral Reductions
    Louis Narmour
    ,
    Tomofumi Yuki
    ,
    Sanjay V. Rajopadhye
  49. 49
    MimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age
    Roland Leißa
    ,
    Marcel Ullrich
    ,
    Joachim Meyer
    ,
    Sebastian Hack
  50. 50
    Model Checking C/C++ with Mixed-Size Accesses
    Iason Marmanis
    ,
    Michalis Kokologiannakis
    ,
    Viktor Vafeiadis