PPaperPicks
← All conferences
Editions202620252024

POPL 2024

A*

ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Official site ↗
93
accepted papers
295
authors
January 17-19, 2024
dates
United Kingdom
location

93 / 93 papers

  1. 1
    A Case for Synthesis of Recursive Quantum Unitary Programs
    Haowei Deng
    ,
    Runzhou Tao
    ,
    Yuxiang Peng
    ,
    Xiaodi Wu
  2. 2
    A Core Calculus for Documents: Or, Lambda: The Ultimate Document
    Will Crichton
    ,
    Shriram Krishnamurthi
  3. 3
    A Formalization of Core Why3 in Coq
    Joshua M. Cohen
    ,
    Philip Johnson-Freyd
  4. 4
    A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verified Proofs of Linearizability
    Prasad Jayanti
    ,
    Siddhartha Jayanti
    ,
    Ugur Y. Yavuz
    ,
    Lizzie Hernandez
  5. 5
    Algebraic Effects Meet Hoare Logic in Cubical Agda
    Donnacha Oisín Kidney
    ,
    Zhixuan Yang
    ,
    Nicolas Wu
  6. 6
    An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic
    Angus Hammond
    ,
    Zongyuan Liu
    ,
    Thibaut Pérami
    ,
    Peter Sewell
    ,
    Lars Birkedal
    ,
    Jean Pichon-Pharabod
  7. 7
    An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification
    Neta Elad
    ,
    Oded Padon
    ,
    Sharon Shoham
  8. 8
    An Iris Instance for Verifying CompCert C Programs
    William Mansky
    ,
    Ke Du
  9. 9
    Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers
    Fuga Kawamata
    ,
    Hiroshi Unno
    ,
    Taro Sekiyama
    ,
    Tachio Terauchi
  10. 10
    API-Driven Program Synthesis for Testing Static Typing Implementations
    Thodoris Sotiropoulos
    ,
    Stefanos Chaliasos
    ,
    Zhendong Su
  11. 11
    Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
    Simon Oddershede Gregersen
    ,
    Alejandro Aguirre
    ,
    Philipp G. Haselwarter
    ,
    Joseph Tassarotti
    ,
    Lars Birkedal
  12. 12
    Automatic Parallelism Management
    Sam Westrick
    ,
    Matthew Fluet
    ,
    Mike Rainey
    ,
    Umut A. Acar
  13. 13
    Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation
    Patrick Cousot
  14. 14
    Coarser Equivalences for Causal Concurrency
    Azadeh Farzan
    ,
    Umang Mathur
  15. 15
    Commutativity Simplifies Proofs of Parameterized Programs
    Azadeh Farzan
    ,
    Dominik Klumpp
    ,
    Andreas Podelski
  16. 16
    Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing
    Jules Jacobs
    ,
    Jonas Kastberg Hinrichsen
    ,
    Robbert Krebbers
  17. 17
    Decalf: A Directed, Effectful Cost-Aware Logical Framework
    Harrison Grodin
    ,
    Yue Niu
    ,
    Jonathan Sterling
    ,
    Robert Harper
  18. 18
    Deciding Asynchronous Hyperproperties for Recursive Programs
    Jens Oliver Gutsfeld
    ,
    Markus Müller-Olm
    ,
    Christoph Ohrem
  19. 19
    Decision and Complexity of Dolev-Yao Hyperproperties
    Itsaka Rakotonirina
    ,
    Gilles Barthe
    ,
    Clara Schneidewind
  20. 20
    Disentanglement with Futures, State, and Interaction
    Jatin Arora
    ,
    Stefan K. Muller
    ,
    Umut A. Acar
  21. 21
    DisLog: A Separation Logic for Disentanglement
    Alexandre Moine
    ,
    Sam Westrick
    ,
    Stephanie Balzer
  22. 22
    EasyBC: A Cryptography-Specific Language for Security Analysis of Block Ciphers against Differential Cryptanalysis
    Pu Sun
    ,
    Fu Song
    ,
    Yuqi Chen
    ,
    Taolue Chen
  23. 23
    Effectful Software Contracts
    Cameron Moy
    ,
    Christos Dimoulas
    ,
    Matthias Felleisen
  24. 24
    Efficient Bottom-Up Synthesis for Programs with Local Variables
    Xiang Li
    ,
    Xiangyu Zhou
    ,
    Rui Dong
    ,
    Yihong Zhang
    ,
    Xinyu Wang
  25. 25
    Efficient CHAD
    Tom Smeding
    ,
    Matthijs Vákár
  26. 26
    Efficient Matching of Regular Expressions with Lookaround Assertions
    Konstantinos Mamouras
    ,
    Agnishom Chattopadhyay
  27. 27
    Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipulations
    Yuantian Ding
    ,
    Xiaokang Qiu
  28. 28
    Enriched Presheaf Model of Quantum FPC
    Takeshi Tsukada
    ,
    Kazuyuki Asada
  29. 29
    Explicit Effects and Effect Constraints in ReML
    Martin Elsman
  30. 30
    Flan: An Expressive and Efficient Datalog Compiler for Program Analysis
    Supun Abeysinghe
    ,
    Anxhelo Xhebraj
    ,
    Tiark Rompf
  31. 31
    Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules
    Ling Zhang
    ,
    Yuting Wang
    ,
    Jinhua Wu
    ,
    Jérémie Koenig
    ,
    Zhong Shao
  32. 32
    Fusing Direct Manipulations into Functional Programs
    Xing Zhang
    ,
    Ruifeng Xie
    ,
    Guanchen Guo
    ,
    Xiao He
    ,
    Tao Zan
    ,
    Zhenjiang Hu
  33. 33
    Generating Well-Typed Terms That Are Not "Useless"
    Justin Frank
    ,
    Benjamin Quiring
    ,
    Leonidas Lampropoulos
  34. 34
    Guided Equality Saturation
    Thomas Koehler
    ,
    Andrés Goens
    ,
    Siddharth Bhat
    ,
    Tobias Grosser
    ,
    Phil Trinder
    ,
    Michel Steuwer
  35. 35
    Higher Order Bayesian Networks, Exactly
    Claudia Faggian
    ,
    Daniele Pautasso
    ,
    Gabriele Vanoni
  36. 36
    How Hard Is Weak-Memory Testing?
    Soham Chakraborty
    ,
    Shankara Narayanan Krishna
    ,
    Umang Mathur
    ,
    Andreas Pavlogiannis
  37. 37
    Ill-Typed Programs Don't Evaluate
    Steven Ramsay
    ,
    Charlie Walpole
  38. 38
    Implementation and Synthesis of Math Library Functions
    Ian Briggs
    ,
    Yash Lad
    ,
    Pavel Panchekha
  39. 39
    Indexed Types for a Statically Safe WebAssembly
    Adam T. Geller
    ,
    Justin Frank
    ,
    William J. Bowman
  40. 40
    Inference of Probabilistic Programs with Moment-Matching Gaussian Mixtures
    Francesca Randone
    ,
    Luca Bortolussi
    ,
    Emilio Incerto
    ,
    Mirco Tribastone
  41. 41
    Inference of Robust Reachability Constraints
    Yanis Sellami
    ,
    Guillaume Girol
    ,
    Frédéric Recoules
    ,
    Damien Couroussé
    ,
    Sébastien Bardin
  42. 42
    Internal and Observational Parametricity for Cubical Agda
    Antoine Van Muylder
    ,
    Andreas Nuyts
    ,
    Dominique Devriese
  43. 43
    Internal Parametricity, without an Interval
    Thorsten Altenkirch
    ,
    Yorgo Chamoun
    ,
    Ambrus Kaposi
    ,
    Michael Shulman
  44. 44
    Internalizing Indistinguishability with Dependent Types
    Yiyun Liu
    ,
    Jonathan Chan
    ,
    Jessica Shi
    ,
    Stephanie Weirich
  45. 45
    Mechanizing Refinement Types
    Michael Borkowski
    ,
    Niki Vazou
    ,
    Ranjit Jhala
  46. 46
    Modular Denotational Semantics for Effects with Guarded Interaction Trees
    Dan Frumin
    ,
    Amin Timany
    ,
    Lars Birkedal
  47. 47
    Monotonicity and the Precision of Program Analysis
    Marco Campion
    ,
    Mila Dalla Preda
    ,
    Roberto Giacobazzi
    ,
    Caterina Urban
  48. 48
    Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions
    Jianan Yao
    ,
    Runzhou Tao
    ,
    Ronghui Gu
    ,
    Jason Nieh
  49. 49
    Nominal Recursors as Epi-Recursors
    Andrei Popescu
  50. 50
    On Learning Polynomial Recursive Programs
    Alex Buna-Marginean
    ,
    Vincent Cheval
    ,
    Mahsa Shirmohammadi
    ,
    James Worrell