POPL 2026
Proceedings of the ACM on Programming Languages, Volume 10, Number POPL

Title Page

Editorial Message

Sponsors

The Complexity of Testing Message-Passing Concurrency
Zheng Shi, Lasse Møldrup, Umang Mathur, and Andreas Pavlogiannis
(National University of Singapore, Singapore; Aarhus University, Denmark)

Publisher's Version Published Artifact Artifacts Available

Let Generalization, Polymorphic Recursion, and Variable Minimization in Boolean-Kinded Type Systems
Joseph A. Zullo
(Purdue University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Normalisation for First-Class Universe Levels
Nils Anders Danielsson, Naïm Camille Favier, and Ondřej Kubánek
(University of Gothenburg and Chalmers University of Technology, Sweden; Chalmers University of Technology and University of Gothenburg, Sweden; Chalmers University of Technology, Sweden)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable ACM SIGPLAN Distinguished Paper Award

Qudit Quantum Programming with Projective Cliffords
Jennifer Paykin and Sam Winnick
(University of Vermont, USA; Intel, USA; Simon Fraser University, Canada; University of Waterloo, Canada)

Publisher's Version

Hadamard-Pi: Equational Quantum Programming
Wang Fang, Chris Heunen, and Robin Kaarsgaard
(University of Edinburgh, UK; University of Southern Denmark, Denmark)

Publisher's Version

RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing
Yusuke Matsushita, Kengo Hirata, Ryo Wakizaka, and Emanuele D'Osualdo
(Kyoto University, Japan; University of Edinburgh, UK; University of Konstanz, Germany)

Publisher's Version

Hyperfunctions: Communicating Continuations
Donnacha Oisín Kidney and Nicolas Wu
(Imperial College London, UK)

Publisher's Version

ArchSem: Reusable Rigorous Semantics of Relaxed Architectures
Thibaut Pérami, Thomas Bauereiss, Brian Campbell, Zongyuan Liu, Nils Lauermann, Alasdair Armstrong, and Peter Sewell
(University of Cambridge, UK; University of Edinburgh, UK; Aarhus University, Denmark)

Publisher's Version

Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants
Noam Zilberstein, Alexandra Silva, and Joseph Tassarotti
(Cornell University, USA; New York University, USA)

Publisher's Version ACM SIGPLAN Distinguished Paper Award

Characterizing Sets of Theories That Can Be Disjointly Combined
Benjamin Przybocki, Guilherme V. Toledo, and Yoni Zohar
(Carnegie Mellon University, USA; Bar-Ilan University, Israel)

Publisher's Version

Local Contextual Type Inference
Xu Xue, Chen Cui, Shengyi Jiang, and Bruno C. d. S. Oliveira
(University of Hong Kong, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

JAX Autodiff from a Linear Logic Perspective
Giulia Giusti and Michele Pagani
(ENS Lyon - CNRS - Université Claude Bernard Lyon 1 - LIP - UMR 5668, France)

Publisher's Version

TypeDis: A Type System for Disentanglement
Alexandre Moine, Stephanie Balzer, Alex Xu, and Sam Westrick
(New York University, USA; Carnegie Mellon University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Network Change Validation with Relational NetKAT
Han Xu, Zachary Kincaid, Ratul Mahajan, and David Walker
(Princeton University, USA; University of Washington, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Typing Strictness
Daniel Sainati, Joseph W. Cutler, Benjamin C. Pierce, and Stephanie Weirich
(University of Pennsylvania, USA)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Functional

An Expressive Assertion Language for Quantum Programs
Bonan Su, Yuan Feng, Mingsheng Ying, and Li Zhou
(Tsinghua University, China; University of Technology Sydney, Australia; Institute of Software at Chinese Academy of Sciences, China)

Publisher's Version

Fuzzing Guided by Bayesian Program Analysis
Yifan Zhang and Xin Zhang
(Peking University, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

ChiSA: Static Analysis for Lightweight Chisel Verification
Jiacai Cui, Qinlin Chen, Zhongsheng Zhan, Tian Tan, and Yue Li
(Nanjing University, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

General Decidability Results for Systems with Continuous Counters
A. R. Balasubramanian, Matthew Hague, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche
(MPI-SWS, Germany; Royal Holloway University of London, UK; Uppsala University, Sweden)

Publisher's Version

Extensible Data Types with Ad-Hoc Polymorphism
Matthew Toohey, Yanning Chen, Ara Jamalzadeh, and Ningning Xie
(University of Toronto, Canada)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Optimising Density Computations in Probabilistic Programs via Automatic Loop Vectorisation
Sangho Lim, Hyoungjin Lim, Wonyeol Lee, Xavier Rival, and Hongseok Yang
(KAIST, Republic of Korea; POSTECH, Republic of Korea; DIENS - École Normale Supérieure de Paris - CNRS - PSL University, France; Inria, France)

Publisher's Version Info

AdapTT: Functoriality for Dependent Type Casts
Arthur Adjedj, Meven Lennon-Bertrand, Thibaut Benjamin, and Kenji Maillard
(ENS Paris-Saclay - Université Paris-Saclay, France; Université Paris Cité - Inria - CNRS - IRIF, France; Université Paris-Saclay - CNRS - ENS Paris-Saclay - LMF, France; Nantes Université - École Centrale Nantes - CNRS - Inria - LS2N - UMR 6004, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Quotient Polymorphism
Brandon Hewer and Graham Hutton
(University of Nottingham, UK)

Publisher's Version Info ACM SIGPLAN Distinguished Paper Award

On Circuit Description Languages, Indexed Monads, and Resource Analysis
Ken Sakayori, Andrea Colledan, and Ugo Dal Lago
(University of Tokyo, Japan; University of Bologna, Italy; Centre Inria d’Université Côte d’Azur, France)

Publisher's Version

Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by Equality Saturation
Marcus Rossel, Rudi Schneider, Thomas Kœhler, Michel Steuwer, and Andrés Goens
(Barkhausen Institut, Germany; TU Darmstadt, Germany; TU Berlin, Germany; ICube Lab - CNRS - Université de Strasbourg, France; University of Amsterdam, Netherlands)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

All for One and One for All: Program Logics for Exploiting Internal Determinism in Parallel Programs
Alexandre Moine, Sam Westrick, and Joseph Tassarotti
(New York University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable ACM SIGPLAN Distinguished Paper Award

Security Reasoning via Substructural Dependency Tracking
Hemant Gouni, Frank Pfenning, and Jonathan Aldrich
(Carnegie Mellon University, USA)

Publisher's Version Published Artifact Artifacts Available ACM SIGPLAN Distinguished Paper Award

Dependent Coeffects for Local Sensitivity Analysis
Victor Sannier and Patrick Baillot
(Univ. Lille - CNRS - Inria - Centrale Lille - UMR 9189 CRIStAL, France)

Publisher's Version

Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions
Neta Elad, Adithya Murali, and Sharon Shoham
(Tel Aviv University, Israel; University of Wisconsin, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Algorithmic Conversion with Surjective Pairing: A Syntactic and Untyped Approach
Yiyun Liu and Stephanie Weirich
(University of Pennsylvania, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Abstraction Functions as Types: Modular Verification of Cost and Behavior in Dependent Type Theory
Harrison Grodin, Runming Li, and Robert Harper
(Carnegie Mellon University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Rows and Capabilities as Modal Effects
Wenhao Tang and Sam Lindley
(University of Edinburgh, UK)

Publisher's Version

Tropical Mathematics and the Lambda-Calculus II: Tropical Geometry of Probabilistic Programming Languages
Davide Barbarossa and Paolo Pistone
(University of Bath, UK; Université Claude Bernard Lyon 1, France)

Publisher's Version

A Relational Separation Logic for Effect Handlers
Paulo Emílio de Vilhena, Simcha van Collem, Ines Wright, and Robbert Krebbers
(Imperial College London, UK; Radboud University Nijmegen, Netherlands; Aarhus University, Denmark)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Compiling to Linear Neurons
Joey Velez-Ginorio, Nada Amin, Konrad Kording, and Steve Zdancewic
(University of Pennsylvania, USA; Harvard University, USA)

Publisher's Version

Handling Higher-Order Effectful Operations with Judgemental Monadic Laws
Zhixuan Yang and Nicolas Wu
(Imperial College London, UK)

Publisher's Version

Accelerating Syntax-Guided Program Synthesis by Optimizing Domain-Specific Languages
Zhentao Ye, Ruyi Ji, Yingfei Xiong, and Xin Zhang
(Peking University, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Parametrised Verification of Intel-x86 Programs
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan
(Uppsala University, Sweden; Mälardalen University, Sweden; IRIF - Université Paris Cité, France; Chennai Mathematical Institute - IRL RelaX, India; Institute of Mathematical Sciences - HBNI - IRL RelaX, India)

Publisher's Version

Handling Scope Checks: A Comparative Framework for Dynamic Scope Extrusion Checks
Michael Lee, Ningning Xie, Oleg Kiselyov, and Jeremy Yallop
(University of Cambridge, UK; University of Toronto, Canada; Tohoku University, Japan)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

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, and Michael Sammler
(MPI-SWS, Germany; IST Austria, Austria)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Arbitration-Free Consistency Is Available (and Vice Versa)
Hagit Attiya, Constantin Enea, and Enrique Román-Calvo
(Technion - Israel Institute of Technology, Israel; LIX - Ecole Polytechnique - CNRS - Institut Polytechnique de Paris, France; University of Freiburg, Germany)

Publisher's Version

The Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs
Frank Schüssele, Matthias Zumkeller, Miriam Lagunes-Rochin, and Dominik Klumpp
(University of Freiburg, Germany; LIX - CNRS - École Polytechnique, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Canonicity for Indexed Inductive-Recursive Types
András Kovács
(University of Gothenburg, Sweden; Chalmers University of Technology, Sweden)

Publisher's Version

Context-Free-Language Reachability for Almost-Commuting Transition Systems
Nikhil Pimpalkhare, Zachary Kincaid, and Thomas Reps
(Princeton University, USA; University of Wisconsin, USA)

Publisher's Version

Recurrence Sets for Proving Fair Non-termination under Axiomatic Memory Consistency Models
Thomas Haas, Roland Meyer, Hernán Ponce de León, and Andrés Lomelí Garduño
(TU Braunschweig, Germany; Huawei Dresden Research Center, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

U-Turn: Enhancing Incorrectness Analysis by Reversing Direction
Flavio Ascari, Roberto Bruni, Roberta Gori, and Azalea Raad
(University of Konstanz, Germany; University of Pisa, Italy; Imperial College London, UK)

Publisher's Version

The Simple Essence of Boolean-Algebraic Subtyping: Semantic Soundness for Algebraic Union, Intersection, Negation, and Equi-recursive Types
Chun Yin Chau and Lionel Parreaux
(Hong Kong University of Science and Technology, Hong Kong)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable

Miri: Practical Undefined Behavior Detection for Rust
Ralf Jung, Benjamin Kimock, Christian Poveda, Eduardo Sánchez Muñoz, Oli Scherer, and Qian Wang
(ETH Zurich, Switzerland; Lansweeper NV, USA; Unaffiliated, Colombia; Unaffiliated, Spain; Unaffiliated, Germany; Unaffiliated, UK)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable

Verifying Almost-Sure Termination for Randomized Distributed Algorithms
Constantin Enea, Rupak Majumdar, Harshit Jitendra Motwani, and V. R. Sathiyanarayana
(LIX - Ecole Polytechnique - Institut Polytechnique de Paris, France; MPI-SWS, Germany)

Publisher's Version

A Synthetic Reconstruction of Multiparty Session Types
David Castro-Perez, Francisco Ferreira, and Sung-Shik Jongmans
(University of Kent, UK; Royal Holloway University of London, UK; University of Groningen, Netherlands)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

A Modular Static Cost Analysis for GPU Warp-Level Parallelism
Gregory Blike, Hannah Zicarelli, Udaya Sathiyamoorthy, Julien Lange, and Tiago Cogumbreiro
(University of Massachusetts at Boston, USA; Royal Holloway University of London, UK)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable

Inductive Program Synthesis by Meta-Analysis-Guided Hole Filling
Doyoon Lee, Woosuk Lee, and Kwangkeun Yi
(Seoul National University, Republic of Korea; Hanyang University, Republic of Korea)

Publisher's Version

A Lazy, Concurrent Convertibility Checker
Nathanaëlle Courant and Xavier Leroy
(OCamlPro, France; Collège de France - PSL University, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Bayesian Separation Logic: A Logical Foundation and Axiomatic Semantics for Probabilistic Programming
Shing Hin Ho, Nicolas Wu, and Azalea Raad
(Imperial College London, UK)

Publisher's Version Info

Higher-Order Behavioural Conformances via Fibrations
Henning Urbat
(Friedrich-Alexander-University Erlangen-Nürnberg, Germany)

Publisher's Version

Determination Problems for Orbit Closures and Matrix Groups
Rida Ait El Manssour, George Kenison, Mahsa Shirmohammadi, Anton Varonka, and James Worrell
(University of Oxford, UK; Liverpool John Moores University, UK; CNRS - IRIF, France; TU Wien, Austria)

Publisher's Version

Domain-Theoretic Semantics for Functional Logic Programming
Eddie Jones, Samson Main, Celia Mengyue Li, Jonathan Marriott, and G. A. Kavvos
(University of Bristol, UK)

Publisher's Version

Consistent Updates for Scalable Microservices
Devora Chait-Roth, Kedar S. Namjoshi, and Thomas Wies
(New York University, USA; Nokia Bell Labs, USA)

Publisher's Version

Zoo: A Framework for the Verification of Concurrent OCaml 5 Programs using Separation Logic
Clément Allain and Gabriel Scherer
(Inria, France; Université Paris Cité, France)

Publisher's Version

The Relative Monadic Metalanguage
Jack Liell-Cock, Zev Shirazi, and Sam Staton
(University of Oxford, UK)

Publisher's Version

Di- is for Directed: First-Order Directed Type Theory via Dinaturality
Andrea Laretto, Fosco Loregian, and Niccolò Veltri
(Tallinn University of Technology, Estonia)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Encode the Cake and Eat It Too: Controlling Computation in Type Theory, Locally
Yann Leray and Théo Winterhalter
(Nantes Université, France; Inria, France; LMF, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable ACM SIGPLAN Distinguished Paper Award

DafnyMPI: A Dafny Library for Verifying Message-Passing Concurrent Programs
Aleksandr Fedchin, Antero Mejr, Hari Sundar, and Jeffrey S. Foster
(Tufts University, USA; American University of Central Asia, Kirghizstan)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

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, and Sam Staton
(University of Edinburgh, UK; University of Oxford, UK)

Publisher's Version ACM SIGPLAN Distinguished Paper Award

A Logic for the Imprecision of Abstract Interpretations
Marco Campion, Mila Dalla Preda, Roberto Giacobazzi, and Caterina Urban
(Inria - ENS - Université PSL, France; University of Verona, Italy; University of Arizona, USA)

Publisher's Version

ChopChop: A Programmable Framework for Semantically Constraining the Output of Language Models
Shaan Nagy, Timothy Zhou, Nadia Polikarpova, and Loris D'Antoni
(University of California at San Diego, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Piecewise Analysis of Probabilistic Programs via 𝑘-Induction
Tengshun Yang, Shenghua Feng, Hongfei Fu, Naijun Zhan, Jingyu Ke, and Shiyang Wu
(Institute of Software at Chinese Academy of Sciences, China; Shanghai Jiao Tong University, China; Peking University, China; Zhongguancun Lab, China)

Publisher's Version Published Artifact Artifacts Available

Formal Verification for JavaScript Regular Expressions: A Proven Mechanized Semantics and Its Applications
Aurèle Barrière, Victor Deng, and Clément Pit-Claudel
(EPFL, Switzerland; École Normale Supérieure - PSL - CNRS, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable ACM SIGPLAN Distinguished Paper Award

Lazy Linearity for a Core Functional Language
Rodrigo Mesquita and Bernardo Toninho
(Well-Typed LLP, UK; Instituto Superior Técnico - University of Lisbon, Portugal; INESC-ID, Portugal)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Parameterized Verification of Quantum Circuits
Parosh Aziz Abdulla, Yu-Fang Chen, Michal Hečko, Lukáš Holík, Ondřej Lengál, Jyun-Ao Lin, and Ramanathan S. Thinniyam
(Uppsala University, Sweden; Mälardalen University, Sweden; Academia Sinica, Taiwan; Brno University of Technology, Czechia; Aalborg University, Denmark; National Taipei University of Technology, Taiwan)

Publisher's Version

A Verified High-Performance Composable Object Library for Remote Direct Memory Access
Guillaume Ambal, George Hodgkins, Mark Madler, Gregory Chockler, Brijesh Dongol, Joseph Izraelevitz, Azalea Raad, and Viktor Vafeiadis
(Imperial College London, UK; University of Colorado, USA; University of Surrey, UK; MPI-SWS, Germany)

Publisher's Version

A Family of Sims with Diverging Interests
Nicolas Chappe
(CNRS - Univ. Grenoble Alpes - Grenoble INP - Verimag, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Classical Notions of Computation and the Hasegawa-Thielecke Theorem
Éléonore Mangel, Paul-André Melliès, and Guillaume Munch-Maccagnoni
(Univ. Paris Cité - CNRS - Inria, France; Inria - LS2N - CNRS, France)

Publisher's Version

Bounded Treewidth, Multiple Context-Free Grammars, and Downward Closures
C. Aiswarya, Pascal Baumann, Prakash Saivasan, Lia Schütze, and Georg Zetzsche
(Chennai Mathematical Institute, India; MPI-SWS, Germany; Institute of Mathematical Sciences - HBNI - IRL RelaX, India)

Publisher's Version

Oriented Metrics for Bottom-Up Enumerative Synthesis
Roland Meyer and Jakob Tepe
(TU Braunschweig, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Big-Stop Semantics: Small-Step Semantics in a Big-Step Judgment
David M. Kahn, Jan Hoffmann, and Runming Li
(Denison University, USA; Carnegie Mellon University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Foundational Multi-Modal Program Verifiers
Vladimir Gladshtein, George Pîrlea, Qiyuan Zhao, Vitaly Kurin, and Ilya Sergey
(National University of Singapore, Singapore; Neapolis University Pafos, Cyprus)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Generating Compilers for Qubit Mapping and Routing
Abtin Molavi, Amanda Xu, Ethan Cecchetti, Swamit Tannu, and Aws Albarghouthi
(University of Wisconsin-Madison, USA)

Publisher's Version

Welterweight Go: Boxing, Structural Subtyping, and Generics
Raymond Hu, Julien Lange, Bernardo Toninho, Philip Wadler, Robert Griesemer, and Keith Randall
(Queen Mary University of London, UK; Royal Holloway University of London, UK; Instituto Superior Técnico - University of Lisbon, Portugal; INESC-ID, Portugal; University of Edinburgh, UK; Google, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Nice to Meet You: Synthesizing Practical MLIR Abstract Transformers
Xuanyu Peng, Dominic Kennedy, Yuyou Fan, Ben Greenman, John Regehr, and Loris D'Antoni
(University of California at San Diego, USA; University of Utah, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Counting and Sampling Traces in Regular Languages
Alexis de Colnet, Kuldeep S. Meel, and Umang Mathur
(TU Wien, Austria; University of Toronto, Canada; National University of Singapore, Singapore)

Publisher's Version

A Complementary Approach to Incorrectness Typing
Celia Mengyue Li, Sophie Pull, and Steven Ramsay
(University of Bristol, UK)

Publisher's Version

From Semantics to Syntax: A Type Theory for Comprehension Categories
Niyousha Najmaei, Niels van der Weide, Benedikt Ahrens, and Paige Randall North
(École Polytechnique, France; Radboud University Nijmegen, Netherlands; Delft University of Technology, Netherlands; Utrecht University, Netherlands)

Publisher's Version

Parameterized Infinite-State Reactive Synthesis
Benedikt Maderbacher and Roderick Bloem
(Graz University of Technology, Austria)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

What Is a Monoid?
Paul Blain Levy and Morgan Rogers
(University of Birmingham, UK; University Sorbonne Paris 13, France)

Publisher's Version

Stateful Differential Operators for Incremental Computing
Runqing Xu and Sebastian Erdweg
(KIT, Germany)

Publisher's Version

Probabilistic Programming with Vectorized Programmable Inference
McCoy R. Becker, Mathieu Huot, George Matheos, Xiaoyan Wang, Karen Chung, Colin Smith, Sam Ritchie, Rif A. Saurous, Alexander K. Lew, Martin C. Rinard, and Vikash K. Mansinghka
(Massachusetts Institute of Technology, USA; Google, USA; Yale University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Cryptis: Cryptographic Reasoning in Separation Logic
Arthur Azevedo de Amorim, Amal Ahmed, and Marco Gaboardi
(Rochester Institute of Technology, USA; Northeastern University, USA; Boston University, USA)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable

Quantum Circuits Are Just a Phase
Chris Heunen, Louis Lemonnier, Christopher McNally, and Alex Rice
(University of Edinburgh, UK; Massachusetts Institute of Technology, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Bounded Sort Polymorphism with Elimination Constraints
Johann Rosain, Tomás Díaz, Kenji Maillard, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter, and Théo Winterhalter
(ENS Lyon, France; University of Chile, Chile; University of Nantes, France; Inria, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Coco: Corecursion with Compositional Heterogeneous Productivity
Jaewoo Kim, Yeonwoo Nam, and Chung-Kil Hur
(Seoul National University, Republic of Korea)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Corrigendum: Unrealizability Logic
Jinwoo Kim, Loris D'Antoni, and Thomas Reps
(University of Wisconsin-Madison, USA)

Publisher's Version