POPL 2024
Proceedings of the ACM on Programming Languages, Volume 8, Number POPL
Powered by
Conference Publishing Consulting

Proceedings of the ACM on Programming Languages, Volume 8, Number POPL, January 14–20, 2024, London, UK

POPL – Journal Issue

Contents - Abstracts - Authors

Frontmatter

Title Page
Editorial Message
POPL 2024 Sponsors and Supporters

Papers

Ramsey Quantifiers in Linear Arithmetics
Pascal Bergsträßer ORCID logo, Moses Ganardi ORCID logo, Anthony W. Lin ORCID logo, and Georg Zetzsche ORCID logo
(University of Kaiserslautern-Landau, Germany; MPI-SWS, Germany)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Deciding Asynchronous Hyperproperties for Recursive Programs
Jens Oliver Gutsfeld ORCID logo, Markus Müller-Olm ORCID logo, and Christoph Ohrem ORCID logo
(University of Münster, Germany)
Publisher's Version
Shoggoth: A Formal Foundation for Strategic Rewriting
Xueying Qin ORCID logo, Liam O’ConnorORCID logo, Rob van Glabbeek ORCID logo, Peter Höfner ORCID logo, Ohad Kammar ORCID logo, and Michel Steuwer ORCID logo
(University of Edinburgh, UK; UNSW, Sydney, Australia; Australian National University, Australia; TU Berlin, Germany)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Reachability in Continuous Pushdown VASS
A. R. Balasubramanian ORCID logo, Rupak Majumdar ORCID logo, Ramanathan S. Thinniyam ORCID logo, and Georg Zetzsche ORCID logo
(MPI-SWS, Germany; Uppsala University, Sweden)
Publisher's Version
Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers
Fuga Kawamata ORCID logo, Hiroshi UnnoORCID logo, Taro SekiyamaORCID logo, and Tachio Terauchi ORCID logo
(Waseda University, Japan; University of Tsukuba, Japan; National Institute of Informatics, Japan)
Publisher's Version Artifacts Reusable
An Iris Instance for Verifying CompCert C Programs
William ManskyORCID logo and Ke Du ORCID logo
(University of Illinois Chicago, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation
Patrick Cousot ORCID logo
(New York University, USA)
Publisher's Version Archive submitted (1.7 MB) Info
Internal and Observational Parametricity for Cubical Agda
Antoine Van Muylder ORCID logo, Andreas Nuyts ORCID logo, and Dominique DevrieseORCID logo
(KU Leuven, Belgium)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
Amin TimanyORCID logo, Simon Oddershede GregersenORCID logo, Léo Stefanesco ORCID logo, Jonas Kastberg Hinrichsen ORCID logo, Léon Gondelman ORCID logo, Abel Nieto ORCID logo, and Lars BirkedalORCID logo
(Aarhus University, Denmark; MPI-SWS, Germany)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Decalf: A Directed, Effectful Cost-Aware Logical Framework
Harrison GrodinORCID logo, Yue Niu ORCID logo, Jonathan Sterling ORCID logo, and Robert HarperORCID logo
(Carnegie Mellon University, USA; University of Cambridge, UK)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
DisLog: A Separation Logic for Disentanglement
Alexandre Moine ORCID logo, Sam WestrickORCID logo, and Stephanie BalzerORCID logo
(Inria, France; Carnegie Mellon University, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Modular Denotational Semantics for Effects with Guarded Interaction Trees
Dan Frumin ORCID logo, Amin TimanyORCID logo, and Lars BirkedalORCID logo
(University of Groningen, Netherlands; Aarhus University, Denmark)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Enriched Presheaf Model of Quantum FPC
Takeshi Tsukada ORCID logo and Kazuyuki Asada ORCID logo
(Chiba University, Japan; Tohoku University, Japan)
Publisher's Version
Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs
Guannan Wei ORCID logo, Oliver Bračevac ORCID logo, Songlin Jia ORCID logo, Yuyan Bao ORCID logo, and Tiark Rompf ORCID logo
(Purdue University, USA; Galois, USA; Augusta University, USA)
Publisher's Version
Nominal Recursors as Epi-Recursors
Andrei Popescu ORCID logo
(University of Sheffield, UK)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Optimal Program Synthesis via Abstract Interpretation
Stephen Mell ORCID logo, Steve ZdancewicORCID logo, and Osbert BastaniORCID logo
(University of Pennsylvania, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Pipelines and Beyond: Graph Types for ADTs with Futures
Francis Rinaldi ORCID logo, june wunder ORCID logo, Arthur Azevedo de Amorim ORCID logo, and Stefan K. Muller ORCID logo
(Illinois Institute of Technology, USA; Boston University, USA; Rochester Institute of Technology, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Programming-by-Demonstration for Long-Horizon Robot Tasks
Noah Patton ORCID logo, Kia Rahmani ORCID logo, Meghana Missula ORCID logo, Joydeep Biswas ORCID logo, and Işıl Dillig ORCID logo
(University of Texas, Austin, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
With a Few Square Roots, Quantum Computing Is as Easy as Pi
Jacques Carette ORCID logo, Chris Heunen ORCID logo, Robin Kaarsgaard ORCID logo, and Amr Sabry ORCID logo
(McMaster University, Canada; University of Edinburgh, UK; University of Southern Denmark, Denmark; Indiana University, USA)
Publisher's Version
The Logical Essence of Well-Bracketed Control Flow
Amin TimanyORCID logo, Armaël GuéneauORCID logo, and Lars BirkedalORCID logo
(Aarhus University, Denmark; Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria - LMF, France)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic
Angus Hammond ORCID logo, Zongyuan Liu ORCID logo, Thibaut Pérami ORCID logo, Peter Sewell ORCID logo, Lars BirkedalORCID logo, and Jean Pichon-Pharabod ORCID logo
(University of Cambridge, UK; Aarhus University, Denmark)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Regular Abstractions for Array Systems
Chih-Duo Hong ORCID logo and Anthony W. Lin ORCID logo
(National Chengchi University, Taiwan; University of Kaiserslautern-Landau, Germany; MPI-SWS, Germany)
Publisher's Version
A Core Calculus for Documents: Or, Lambda: The Ultimate Document
Will Crichton ORCID logo and Shriram Krishnamurthi ORCID logo
(Brown University, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
The Essence of Generalized Algebraic Data Types
Filip Sieczkowski ORCID logo, Sergei Stepanenko ORCID logo, Jonathan Sterling ORCID logo, and Lars BirkedalORCID logo
(Heriot-Watt University, UK; Aarhus University, Denmark; University of Cambridge, UK)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Solvable Polynomial Ideals: The Ideal Reflection for Program Analysis
John Cyphert ORCID logo and Zachary Kincaid ORCID logo
(University of Wisconsin-Madison, USA; Princeton University, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
Simon Oddershede GregersenORCID logo, Alejandro Aguirre ORCID logo, Philipp G. Haselwarter ORCID logo, Joseph Tassarotti ORCID logo, and Lars BirkedalORCID logo
(Aarhus University, Denmark; New York University, USA)
Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable
Quotient Haskell: Lightweight Quotient Types for All
Brandon Hewer ORCID logo and Graham Hutton ORCID logo
(University of Nottingham, UK)
Publisher's Version
Semantic Code Refactoring for Abstract Data Types
Shankara Pailoor ORCID logo, Yuepeng Wang ORCID logo, and Işıl Dillig ORCID logo
(University of Texas, Austin, USA; Simon Fraser University, Canada)
Publisher's Version
EasyBC: A Cryptography-Specific Language for Security Analysis of Block Ciphers against Differential Cryptanalysis
Pu Sun ORCID logo, Fu SongORCID logo, Yuqi Chen ORCID logo, and Taolue Chen ORCID logo
(ShanghaiTech University, China; Institute of Software at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; Birkbeck University of London, UK)
Publisher's Version Info
Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs
Julian Müllner ORCID logo, Marcel MoosbruggerORCID logo, and Laura Kovács ORCID logo
(TU Wien, Austria)
Publisher's Version
Coarser Equivalences for Causal Concurrency
Azadeh FarzanORCID logo and Umang Mathur ORCID logo
(University of Toronto, Canada; National University of Singapore, Singapore)
Publisher's Version
Implementation and Synthesis of Math Library Functions
Ian Briggs ORCID logo, Yash Lad ORCID logo, and Pavel PanchekhaORCID logo
(University of Utah, USA)
Publisher's Version
An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification
Neta Elad ORCID logo, Oded Padon ORCID logo, and Sharon Shoham ORCID logo
(Tel Aviv University, Israel; VMware Research, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
On Learning Polynomial Recursive Programs
Alex Buna-Marginean ORCID logo, Vincent Cheval ORCID logo, Mahsa Shirmohammadi ORCID logo, and James Worrell ORCID logo
(University of Oxford, UK; CNRS - IRIF - Université Paris Cité, France)
Publisher's Version
Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions
Jianan Yao ORCID logo, Runzhou Tao ORCID logo, Ronghui GuORCID logo, and Jason Nieh ORCID logo
(Columbia University, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Efficient CHAD
Tom J. Smeding ORCID logo and Matthijs I. L. Vákár ORCID logo
(Utrecht University, Netherlands)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Positive Almost-Sure Termination: Complexity and Proof Rules
Rupak Majumdar ORCID logo and V. R. Sathiyanarayana ORCID logo
(MPI-SWS, Germany)
Publisher's Version
Automatic Parallelism Management
Sam WestrickORCID logo, Matthew Fluet ORCID logo, Mike Rainey ORCID logo, and Umut A. Acar ORCID logo
(Carnegie Mellon University, USA; Rochester Institute of Technology, USA)
Publisher's Version
Orthologic with Axioms
Simon GuilloudORCID logo and Viktor Kunčak ORCID logo
(EPFL, Switzerland)
Publisher's Version
Polymorphic Type Inference for Dynamic Languages
Giuseppe Castagna ORCID logo, Mickaël Laurent ORCID logo, and Kim Nguyễn ORCID logo
(CNRS - Université Paris Cité, France; Université Paris Cité, France; Université Paris-Saclay, France)
Publisher's Version Published Artifact Archive submitted (1.1 MB) Artifacts Available Artifacts Reusable
Fusing Direct Manipulations into Functional Programs
Xing ZhangORCID logo, Ruifeng Xie ORCID logo, Guanchen Guo ORCID logo, Xiao He ORCID logo, Tao Zan ORCID logo, and Zhenjiang Hu ORCID logo
(Peking University, China; University of Science and Technology Beijing, China; Longyan University, China)
Publisher's Version Published Artifact Video Artifacts Available Artifacts Reusable
On-the-Fly Static Analysis via Dynamic Bidirected Dyck Reachability
Shankaranarayanan Krishna ORCID logo, Aniket Lal ORCID logo, Andreas PavlogiannisORCID logo, and Omkar Tuppe ORCID logo
(IIT Bombay, India; Aarhus University, Denmark)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Quantum Bisimilarity via Barbs and Contexts: Curbing the Power of Non-deterministic Observers
Lorenzo Ceragioli ORCID logo, Fabio GadducciORCID logo, Giuseppe Lomurno ORCID logo, and Gabriele Tedeschi ORCID logo
(IMT School for Advanced Studies Lucca, Italy; University of Pisa, Italy)
Publisher's Version
Internalizing Indistinguishability with Dependent Types
Yiyun Liu ORCID logo, Jonathan Chan ORCID logo, Jessica Shi ORCID logo, and Stephanie Weirich ORCID logo
(University of Pennsylvania, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Polyregular Functions on Unordered Trees of Bounded Height
Mikołaj Bojańczyk ORCID logo and Bartek Klin ORCID logo
(University of Warsaw, Poland; University of Oxford, UK)
Publisher's Version
The Complex(ity) Landscape of Checking Infinite Descent
Liron Cohen ORCID logo, Adham Jabarin ORCID logo, Andrei Popescu ORCID logo, and Reuben N. S. Rowe ORCID logo
(Ben-Gurion University of the Negev, Israel; University of Sheffield, UK; Royal Holloway University of London, UK)
Publisher's Version Published Artifact Archive submitted (300 kB) Artifacts Available Artifacts Reusable
Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing
Jules JacobsORCID logo, Jonas Kastberg Hinrichsen ORCID logo, and Robbert KrebbersORCID logo
(Radboud University Nijmegen, Netherlands; Aarhus University, Denmark)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class Polymorphism
Lionel Parreaux ORCID logo, Aleksander Boruch-Gruszecki ORCID logo, Andong Fan ORCID logo, and Chun Yin Chau ORCID logo
(Hong Kong University of Science and Technology, Hong Kong; EPFL, Switzerland)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Validation of Modern JSON Schema: Formalization and Complexity
Lyes Attouche ORCID logo, Mohamed-Amine Baazizi ORCID logo, Dario Colazzo ORCID logo, Giorgio Ghelli ORCID logo, Carlo Sartiani ORCID logo, and Stefanie Scherzinger ORCID logo
(Université Paris-Dauphine - PSL, France; Sorbonne University, France; University of Pisa, Italy; University of Basilicata, Italy; University of Passau, Germany)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
Thunks and Debits in Separation Logic with Time Credits
François PottierORCID logo, Armaël GuéneauORCID logo, Jacques-Henri Jourdan ORCID logo, and Glen Mével ORCID logo
(Inria, France; Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria - LMF, France; Université Paris-Saclay - CNRS - ENS Paris-Saclay - LMF, France)
Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable
Unboxed Data Constructors: Or, How cpp Decides a Halting Problem
Nicolas Chataing ORCID logo, Stephen Dolan ORCID logo, Gabriel Scherer ORCID logo, and Jeremy YallopORCID logo
(ENS Paris, France; Jane Street, UK; Inria, France; University of Cambridge, UK)
Publisher's Version
Efficient Bottom-Up Synthesis for Programs with Local Variables
Xiang Li ORCID logo, Xiangyu Zhou ORCID logo, Rui Dong ORCID logo, Yihong Zhang ORCID logo, and Xinyu Wang ORCID logo
(University of Michigan, USA; University of Washington, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Disentanglement with Futures, State, and Interaction
Jatin Arora ORCID logo, Stefan K. Muller ORCID logo, and Umut A. Acar ORCID logo
(Carnegie Mellon University, USA; Illinois Institute of Technology, USA)
Publisher's Version
Soundly Handling Linearity
Wenhao TangORCID logo, Daniel HillerströmORCID logo, Sam Lindley ORCID logo, and J. Garrett Morris ORCID logo
(University of Edinburgh, UK; Huawei Zurich Research Center, Switzerland; University of Iowa, USA)
Publisher's Version Published Artifact Archive submitted (1.5 MB) Artifacts Available Artifacts Reusable
Monotonicity and the Precision of Program Analysis
Marco CampionORCID logo, Mila Dalla PredaORCID logo, Roberto GiacobazziORCID logo, and Caterina UrbanORCID logo
(Inria - ENS - Université PSL, Paris, France; University of Verona, Italy; University of Arizona, Tucson, USA)
Publisher's Version
Algebraic Effects Meet Hoare Logic in Cubical Agda
Donnacha Oisín KidneyORCID logo, Zhixuan YangORCID logo, and Nicolas WuORCID logo
(Imperial College London, UK)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Solving Infinite-State Games via Acceleration
Philippe Heim ORCID logo and Rayna Dimitrova ORCID logo
(CISPA Helmholtz Center for Information Security, Germany)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Guided Equality Saturation
Thomas Kœhler ORCID logo, Andrés Goens ORCID logo, Siddharth Bhat ORCID logo, Tobias Grosser ORCID logo, Phil Trinder ORCID logo, and Michel Steuwer ORCID logo
(Inria, France; ICube lab - Université de Strasbourg - CNRS, France; University of Amsterdam, Netherlands; University of Edinburgh, UK; University of Cambridge, UK; University of Glasgow, UK; TU Berlin, Germany)
Publisher's Version Archive submitted (150 kB)
A Case for Synthesis of Recursive Quantum Unitary Programs
Haowei Deng ORCID logo, Runzhou Tao ORCID logo, Yuxiang Peng ORCID logo, and Xiaodi Wu ORCID logo
(University of Maryland, College Park, USA; Columbia University, USA; University of Maryland, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
A Formalization of Core Why3 in Coq
Joshua M. Cohen ORCID logo and Philip Johnson-Freyd ORCID logo
(Princeton University, USA; Sandia National Laboratories, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Probabilistic Programming Interfaces for Random Graphs: Markov Categories, Graphons, and Nominal Sets
Nate Ackerman ORCID logo, Cameron E. Freer ORCID logo, Younesse KaddarORCID logo, Jacek Karwowski ORCID logo, Sean Moss ORCID logo, Daniel RoyORCID logo, Sam StatonORCID logo, and Hongseok YangORCID logo
(Harvard University, USA; Massachusetts Institute of Technology, USA; University of Oxford, UK; University of Birmingham, UK; University of Toronto, Canada; KAIST, South Korea)
Publisher's Version
API-Driven Program Synthesis for Testing Static Typing Implementations
Thodoris Sotiropoulos ORCID logo, Stefanos Chaliasos ORCID logo, and Zhendong Su ORCID logo
(ETH Zurich, Switzerland; Imperial College London, UK)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Inference of Probabilistic Programs with Moment-Matching Gaussian Mixtures
Francesca Randone ORCID logo, Luca Bortolussi ORCID logo, Emilio Incerto ORCID logo, and Mirco TribastoneORCID logo
(IMT School for Advanced Studies Lucca, Italy; University of Trieste, Italy)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Decision and Complexity of Dolev-Yao Hyperproperties
Itsaka Rakotonirina ORCID logo, Gilles Barthe ORCID logo, and Clara Schneidewind ORCID logo
(MPI-SP, Germany; IMDEA Software Institute, Spain)
Publisher's Version
Parikh’s Theorem Made Symbolic
Matthew Hague ORCID logo, Artur Jeż ORCID logo, and Anthony W. Lin ORCID logo
(Royal Holloway University of London, UK; University of Wrocław, Poland; University of Kaiserslautern-Landau, Germany; MPI-SWS, Germany)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
How Hard Is Weak-Memory Testing?
Soham Chakraborty ORCID logo, Shankara Narayanan Krishna ORCID logo, Umang Mathur ORCID logo, and Andreas PavlogiannisORCID logo
(TU Delft, Netherlands; IIT Bombay, India; National University of Singapore, Singapore; Aarhus University, Denmark)
Publisher's Version
Ill-Typed Programs Don’t Evaluate
Steven Ramsay ORCID logo and Charlie Walpole ORCID logo
(University of Bristol, UK)
Publisher's Version
Total Type Error Localization and Recovery with Holes
Eric Zhao ORCID logo, Raef MaroofORCID logo, Anand Dukkipati ORCID logo, Andrew BlinnORCID logo, Zhiyi Pan ORCID logo, and Cyrus OmarORCID logo
(University of Michigan, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
VST-A: A Foundationally Sound Annotation Verifier
Litao Zhou ORCID logo, Jianxing Qin ORCID logo, Qinshi Wang ORCID logo, Andrew W. AppelORCID logo, and Qinxiang Cao ORCID logo
(Shanghai Jiao Tong University, China; University of Hong Kong, China; Princeton University, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Mechanizing Refinement Types
Michael H. Borkowski ORCID logo, Niki VazouORCID logo, and Ranjit Jhala ORCID logo
(University of California, San Diego, USA; IMDEA Software Institute, Spain)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipulations
Yuantian Ding ORCID logo and Xiaokang QiuORCID logo
(Purdue University, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules
Ling Zhang ORCID logo, Yuting Wang ORCID logo, Jinhua Wu ORCID logo, Jérémie Koenig ORCID logo, and Zhong Shao ORCID logo
(Shanghai Jiao Tong University, China; Yale University, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Predictive Monitoring against Pattern Regular Languages
Zhendong Ang ORCID logo and Umang Mathur ORCID logo
(National University of Singapore, Singapore)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Securing Verified IO Programs Against Unverified Code in F*
Cezar-Constantin Andrici ORCID logo, Ștefan Ciobâcă ORCID logo, Cătălin Hriţcu ORCID logo, Guido Martínez ORCID logo, Exequiel Rivas ORCID logo, Éric TanterORCID logo, and Théo Winterhalter ORCID logo
(MPI-SP, Germany; Alexandru Ioan Cuza University, Iași, Romania; Microsoft Research, USA; Tallinn University of Technology, Estonia; University of Chile, Chile; Inria, France)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
ReLU Hull Approximation
Zhongkui Ma ORCID logo, Jiaying LiORCID logo, and Guangdong Bai ORCID logo
(University of Queensland, Australia; Microsoft, China)
Publisher's Version
Polynomial Time and Dependent Types
Robert AtkeyORCID logo
(University of Strathclyde, UK)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
Generating Well-Typed Terms That Are Not “Useless”
Justin Frank ORCID logo, Benjamin Quiring ORCID logo, and Leonidas LampropoulosORCID logo
(University of Maryland, College Park, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Internal Parametricity, without an Interval
Thorsten Altenkirch ORCID logo, Yorgo Chamoun ORCID logo, Ambrus Kaposi ORCID logo, and Michael Shulman ORCID logo
(University of Nottingham, UK; École Polytechnique, France; Eötvös Loránd University, Hungary; University of San Diego, USA)
Publisher's Version
Explicit Effects and Effect Constraints in ReML
Martin Elsman ORCID logo
(University of Copenhagen, Denmark)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Indexed Types for a Statically Safe WebAssembly
Adam T. Geller ORCID logo, Justin Frank ORCID logo, and William J. Bowman ORCID logo
(University of British Columbia, Canada; University of Maryland, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
SimuQ: A Framework for Programming Quantum Hamiltonian Simulation with Analog Compilation
Yuxiang Peng ORCID logo, Jacob Young ORCID logo, Pengyu Liu ORCID logo, and Xiaodi Wu ORCID logo
(University of Maryland, USA; Carnegie Mellon University, USA)
Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable
A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verified Proofs of Linearizability
Prasad Jayanti ORCID logo, Siddhartha Jayanti ORCID logo, Ugur Y. Yavuz ORCID logo, and Lizzie Hernandez ORCID logo
(Dartmouth College, USA; Google Research, USA; Boston University, USA; Microsoft, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Commutativity Simplifies Proofs of Parameterized Programs
Azadeh FarzanORCID logo, Dominik Klumpp ORCID logo, and Andreas Podelski ORCID logo
(University of Toronto, Canada; University of Freiburg, Germany)
Publisher's Version Published Artifact Artifacts Available
Higher Order Bayesian Networks, Exactly
Claudia Faggian ORCID logo, Daniele Pautasso ORCID logo, and Gabriele Vanoni ORCID logo
(IRIF - CNRS - Université Paris Cité, France; University of Turin, Italy)
Publisher's Version
Sound Gradual Verification with Symbolic Execution
Conrad Zimmerman ORCID logo, Jenna DiVincenzo ORCID logo, and Jonathan AldrichORCID logo
(Brown University, USA; Purdue University, USA; Carnegie Mellon University, USA)
Publisher's Version Info
Flan: An Expressive and Efficient Datalog Compiler for Program Analysis
Supun Abeysinghe ORCID logo, Anxhelo Xhebraj ORCID logo, and Tiark Rompf ORCID logo
(Purdue University, USA)
Publisher's Version
On Model-Checking Higher-Order Effectful Programs
Ugo Dal LagoORCID logo and Alexis Ghyselen ORCID logo
(University of Bologna, Italy)
Publisher's Version
Effectful Software Contracts
Cameron Moy ORCID logo, Christos Dimoulas ORCID logo, and Matthias Felleisen ORCID logo
(PLT at Northeastern University, USA; PLT at Northwestern University, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Type-Based Gradual Typing Performance Optimization
John Peter Campora ORCID logo, Mohammad Wahiduzzaman Khan ORCID logo, and Sheng Chen ORCID logo
(Quantinuum, USA; University of Louisiana, Lafayette, USA)
Publisher's Version
Parametric Subtyping for Structural Parametric Polymorphism
Henry DeYoung ORCID logo, Andreia MordidoORCID logo, Frank Pfenning ORCID logo, and Ankush Das ORCID logo
(Carnegie Mellon University, USA; Universidade de Lisboa, Portugal; Amazon, USA)
Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable
Inference of Robust Reachability Constraints
Yanis Sellami ORCID logo, Guillaume Girol ORCID logo, Frédéric Recoules ORCID logo, Damien Couroussé ORCID logo, and Sébastien BardinORCID logo
(Université Grenoble-Alpes - CEA - List, France; Université Paris-Saclay - CEA - List, France)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Efficient Matching of Regular Expressions with Lookaround Assertions
Konstantinos Mamouras ORCID logo and Agnishom Chattopadhyay ORCID logo
(Rice University, USA)
Publisher's Version
Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs
Kevin Batz ORCID logo, Tom Jannik Biskup ORCID logo, Joost-Pieter Katoen ORCID logo, and Tobias Winkler ORCID logo
(RWTH Aachen University, Germany)
Publisher's Version

proc time: 42.86