POPL 2023
Proceedings of the ACM on Programming Languages, Volume 7, Number POPL

Title Page

Article: popl23foreword-fm000-p (type: Frontmatter) doi:

Editorial Message

Article: popl23foreword-fm001-p (type: Frontmatter) doi:

Sponsors

Article: popl23foreword-fm003-p (type: Frontmatter) doi:

CN: Verifying Systems C Code with Separation-Logic Refinement Types
Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, and Neel Krishnaswami
(University of Cambridge, UK)

Publisher's Version Article: popl23main-p2-p (type: Full Paper) doi:10.1145/3571194

Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice
Alejandro Aguirre and Lars Birkedal
(Aarhus University, Denmark)

Publisher's Version Article: popl23main-p3-p (type: Full Paper) doi:10.1145/3571195

A Type-Based Approach to Divide-and-Conquer Recursion in Coq
Pedro Abreu, Benjamin Delaware, Alex Hubers, Christa Jenkins, J. Garrett Morris, and Aaron Stump
(Purdue University, USA; University of Iowa, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p17-p (type: Full Paper) doi:10.1145/3571196

Comparative Synthesis: Learning Near-Optimal Network Designs by Query
Yanjun Wang, Zixuan Li, Chuan Jiang, Xiaokang Qiu, and Sanjay Rao
(Purdue University, USA)

Publisher's Version Archive submitted (1.3 MB) Artifacts Functional Article: popl23main-p33-p (type: Full Paper) doi:10.1145/3571197

ADEV: Sound Automatic Differentiation of Expected Values of Probabilistic Programs
Alexander K. Lew, Mathieu Huot, Sam Staton, and Vikash K. Mansinghka
(Massachusetts Institute of Technology, USA; University of Oxford, UK)

Publisher's Version Archive submitted (1 MB) Article: popl23main-p48-p (type: Full Paper) doi:10.1145/3571198

HFL(Z) Validity Checking for Automated Program Verification
Naoki Kobayashi, Kento Tanahashi, Ryosuke Sato, and Takeshi Tsukada
(University of Tokyo, Japan; Chiba University, Japan)

Publisher's Version Article: popl23main-p55-p (type: Full Paper) doi:10.1145/3571199

From SMT to ASP: Solver-Based Approaches to Solving Datalog Synthesis-as-Rule-Selection Problems
Aaron Bembenek, Michael Greenberg, and Stephen Chong
(Harvard University, USA; Stevens Institute of Technology, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p63-p (type: Full Paper) doi:10.1145/3571200

Why Are Proofs Relevant in Proof-Relevant Models?
Axel Kerinec, Giulio Manzonetto, and Federico Olimpieri
(Université Sorbonne Paris Nord, France; LIPN, France; CNRS, France; University of Leeds, UK)

Publisher's Version Article: popl23main-p66-p (type: Full Paper) doi:10.1145/3571201

Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler
Aurèle Barrière, Sandrine Blazy, and David Pichardie
(University of Rennes, France; Inria, France; CNRS, France; IRISA, France; Meta, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p72-p (type: Full Paper) doi:10.1145/3571202

On the Expressive Power of String Constraints
Joel D. Day, Vijay Ganesh, Nathan Grewal, and Florin Manea
(Loughborough University, UK; University of Waterloo, Canada; University of Göttingen, Germany)

Publisher's Version Article: popl23main-p75-p (type: Full Paper) doi:10.1145/3571203

Proto-Quipper with Dynamic Lifting
Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger
(Dalhousie University, Canada; University of Illinois at Urbana-Champaign, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p79-p (type: Full Paper) doi:10.1145/3571204

Smoothness Analysis for Probabilistic Programs with Application to Optimised Variational Inference
Wonyeol Lee, Xavier Rival, and Hongseok Yang
(Stanford University, USA; Inria, France; ENS, France; CNRS, France; PSL University, France; KAIST, South Korea; IBS, South Korea)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p85-p (type: Full Paper) doi:10.1145/3571205

Executing Microservice Applications on Serverless, Correctly
Konstantinos Kallas, Haoran Zhang, Rajeev Alur, Sebastian Angel, and Vincent Liu
(University of Pennsylvania, USA; Microsoft Research, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl23main-p93-p (type: Full Paper) doi:10.1145/3571206

babble: Learning Better Abstractions with E-Graphs and Anti-unification
David Cao, Rose Kunkel, Chandrakana Nandi, Max Willsey, Zachary Tatlock, and Nadia Polikarpova
(University of California at San Diego, USA; Certora, USA; University of Washington, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p94-p (type: Full Paper) doi:10.1145/3571207

MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code
Alexandra E. Michael, Anitha Gollamudi, Jay Bosamiya, Evan Johnson, Aidan Denlinger, Craig Disselkoen, Conrad Watt, Bryan Parno, Marco Patrignani, Marco Vassena, and Deian Stefan
(University of California at San Diego, USA; University of Washington, USA; University of Massachusetts Lowell, USA; Carnegie Mellon University, USA; Arm, USA; University of Cambridge, UK; University of Trento, Italy; Utrecht University, Netherlands)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl23main-p96-p (type: Full Paper) doi:10.1145/3571208

Grisette: Symbolic Compilation as a Functional Programming Library
Sirui Lu and Rastislav Bodík
(University of Washington, USA; Google Research, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p97-p (type: Full Paper) doi:10.1145/3571209

Locally Nameless Sets
Andrew M. Pitts
(University of Cambridge, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p106-p (type: Full Paper) doi:10.1145/3571210

A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F⋈
Nick Rioux, Xuejing Huang, Bruno C. d. S. Oliveira, and Steve Zdancewic
(University of Pennsylvania, USA; University of Hong Kong, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p111-p (type: Full Paper) doi:10.1145/3571211

Kater: Automating Weak Memory Model Metatheory and Consistency Checking
Michalis Kokologiannakis, Ori Lahav, and Viktor Vafeiadis
(MPI-SWS, Germany; Tel Aviv University, Israel)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p112-p (type: Full Paper) doi:10.1145/3571212

An Algebra of Alignment for Relational Verification
Timos Antonopoulos, Eric Koskinen, Ton Chanh Le, Ramana Nagasamudram, David A. Naumann, and Minh Ngo
(Yale University, USA; Stevens Institute of Technology, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p114-p (type: Full Paper) doi:10.1145/3571213

Optimal CHC Solving via Termination Proofs
Yu Gu, Takeshi Tsukada, and Hiroshi Unno
(University of Tsukuba, Japan; Chiba University, Japan; RIKEN AIP, Japan)

Publisher's Version Article: popl23main-p115-p (type: Full Paper) doi:10.1145/3571214

Towards a Higher-Order Mathematical Operational Semantics
Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat
(University of Erlangen-Nuremberg, Germany)

Publisher's Version Article: popl23main-p119-p (type: Full Paper) doi:10.1145/3571215

Unrealizability Logic
Jinwoo Kim, Loris D'Antoni, and Thomas Reps
(University of Wisconsin-Madison, USA; Seoul National University, South Korea)

Publisher's Version Article: popl23main-p120-p (type: Full Paper) doi:10.1145/3571216

Version of Record: Version of Record to "Unrealizability Logic" by Jinwoo Kim, Loris D’Antoni, and Thomas Reps, published in Proc. ACM Program. Lang. 7, POPL, Article 23 (January 2023), https://doi.org/10.1145/3571216.

The Geometry of Causality: Multi-token Geometry of Interaction and Its Causal Unfolding
Simon Castellan and Pierre Clairambault
(University of Rennes, France; Inria, France; CNRS, France; IRISA, France; Université Aix-Marseille, France; Université de Toulon, France; LIS, France)

Publisher's Version Artifacts Functional Article: popl23main-p121-p (type: Full Paper) doi:10.1145/3571217

A High-Level Separation Logic for Heap Space under Garbage Collection
Alexandre Moine, Arthur Charguéraud, and François Pottier
(Inria, France; Université de Strasbourg, France; CNRS, France; ICube, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p141-p (type: Full Paper) doi:10.1145/3571218

The Path to Durable Linearizability
Emanuele D'Osualdo, Azalea Raad, and Viktor Vafeiadis
(MPI-SWS, Germany; Imperial College London, UK)

Publisher's Version Article: popl23main-p144-p (type: Full Paper) doi:10.1145/3571219

DimSum: A Decentralized Approach to Multi-language Semantics and Verification
Michael Sammler, Simon Spies, Youngju Song, Emanuele D'Osualdo, Robbert Krebbers, Deepak Garg, and Derek Dreyer
(MPI-SWS, Germany; Radboud University Nijmegen, Netherlands)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p145-p (type: Full Paper) doi:10.1145/3571220

A General Noninterference Policy for Polynomial Time
Emmanuel Hainry and Romain Péchoux
(Université de Lorraine, France; CNRS, France; Inria, France; LORIA, France)

Publisher's Version Article: popl23main-p149-p (type: Full Paper) doi:10.1145/3571221

CoqQ: Foundational Verification of Quantum Programs
Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, and Mingsheng Ying
(MPI-SP, Germany; Institute of Software at Chinese Academy of Sciences, China; IMDEA Software Institute, Spain; Meta, France; University of Chinese Academy of Sciences, China; Tsinghua University, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p163-p (type: Full Paper) doi:10.1145/3571222

A Core Calculus for Equational Proofs of Cryptographic Protocols
Joshua Gancher, Kristina Sojakova, Xiong Fan, Elaine Shi, and Greg Morrisett
(Carnegie Mellon University, USA; Inria, France; Rutgers University, USA; Cornell University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p185-p (type: Full Paper) doi:10.1145/3571223

Making a Type Difference: Subtraction on Intersection Types as Generalized Record Operations
Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira
(Peking University, China; University of Hong Kong, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p191-p (type: Full Paper) doi:10.1145/3571224

Qunity: A Unified Language for Quantum and Classical Computing
Finn Voichick, Liyi Li, Robert Rand, and Michael Hicks
(University of Maryland, USA; University of Chicago, USA; Amazon, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p197-p (type: Full Paper) doi:10.1145/3571225

FlashFill++: Scaling Programming by Example by Cutting to the Chase
José Cambronero, Sumit Gulwani, Vu Le, Daniel Perelman, Arjun Radhakrishna, Clint Simon, and Ashish Tiwari
(Microsoft, USA)

Publisher's Version Article: popl23main-p198-p (type: Full Paper) doi:10.1145/3571226

Witnessability of Undecidable Problems
Shuo Ding and Qirun Zhang
(Georgia Institute of Technology, USA)

Publisher's Version Article: popl23main-p218-p (type: Full Paper) doi:10.1145/3571227

Single-Source-Single-Target Interleaved-Dyck Reachability via Integer Linear Programming
Yuanbo Li, Qirun Zhang, and Thomas Reps
(Georgia Institute of Technology, USA; University of Wisconsin-Madison, USA)

Publisher's Version Article: popl23main-p222-p (type: Full Paper) doi:10.1145/3571228

Higher-Order Leak and Deadlock Free Locks
Jules Jacobs and Stephanie Balzer
(Radboud University Nijmegen, Netherlands; Carnegie Mellon University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p231-p (type: Full Paper) doi:10.1145/3571229

A Robust Theory of Series Parallel Graphs
Rajeev Alur, Caleb Stanford, and Christopher Watson
(University of Pennsylvania, USA; University of California at San Diego, USA; University of California at Davis, USA)

Publisher's Version Article: popl23main-p256-p (type: Full Paper) doi:10.1145/3571230

A Compositional Theory of Linearizability
Arthur Oliveira Vale, Zhong Shao, and Yixuan Chen
(Yale University, USA)

Publisher's Version Article: popl23main-p263-p (type: Full Paper) doi:10.1145/3571231

Conditional Contextual Refinement
Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Sammler, and Derek Dreyer
(Seoul National University, South Korea; MPI-SWS, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p264-p (type: Full Paper) doi:10.1145/3571232

Tail Recursion Modulo Context: An Equational Approach
Daan Leijen and Anton Lorenzen
(Microsoft Research, USA; University of Edinburgh, UK)

Publisher's Version Article: popl23main-p271-p (type: Full Paper) doi:10.1145/3571233

Top-Down Synthesis for Library Learning
Matthew Bowers, Theo X. Olausson, Lionel Wong, Gabriel Grand, Joshua B. Tenenbaum, Kevin Ellis, and Armando Solar-Lezama
(Massachusetts Institute of Technology, USA; Cornell University, USA)

Publisher's Version Published Artifact Archive submitted (1.6 MB) Artifacts Available Artifacts Reusable Article: popl23main-p278-p (type: Full Paper) doi:10.1145/3571234

Admissible Types-to-PERs Relativization in Higher-Order Logic
Andrei Popescu and Dmitriy Traytel
(University of Sheffield, UK; University of Copenhagen, Denmark)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p299-p (type: Full Paper) doi:10.1145/3571235

You Only Linearize Once: Tangents Transpose to Gradients
Alexey Radul, Adam Paszke, Roy Frostig, Matthew J. Johnson, and Dougal Maclaurin
(Google Research, USA; Google Research, Poland)

Publisher's Version Article: popl23main-p303-p (type: Full Paper) doi:10.1145/3571236

When Less Is More: Consequence-Finding in a Weak Theory of Arithmetic
Zachary Kincaid, Nicolas Koh, and Shaowei Zhu
(Princeton University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p305-p (type: Full Paper) doi:10.1145/3571237

Dynamic Race Detection with O(1) Samples
Mosaad Al Thokair, Minjian Zhang, Umang Mathur, and Mahesh Viswanathan
(University of Illinois at Urbana-Champaign, USA; National University of Singapore, Singapore)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p314-p (type: Full Paper) doi:10.1145/3571238

Affine Monads and Lazy Structures for Bayesian Programming
Swaraj Dash, Younesse Kaddar, Hugo Paquet, and Sam Staton
(University of Oxford, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p324-p (type: Full Paper) doi:10.1145/3571239

Dargent: A Silver Bullet for Verified Data Layout Refinement
Zilin Chen, Ambroise Lafont, Liam O'Connor, Gabriele Keller, Craig McLaughlin, Vincent Jackson, and Christine Rizkallah
(UNSW, Australia; University of Cambridge, UK; University of Edinburgh, UK; Utrecht University, Netherlands; University of Melbourne, Australia)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p325-p (type: Full Paper) doi:10.1145/3571240

Recursive Subtyping for All
Litao Zhou, Yaoda Zhou, and Bruno C. d. S. Oliveira
(University of Hong Kong, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p335-p (type: Full Paper) doi:10.1145/3571241

Stratified Commutativity in Verification Algorithms for Concurrent Programs
Azadeh Farzan, Dominik Klumpp, and Andreas Podelski
(University of Toronto, Canada; University of Freiburg, Germany)

Publisher's Version Archive submitted (780 kB) Article: popl23main-p348-p (type: Full Paper) doi:10.1145/3571242

Type-Preserving, Dependence-Aware Guide Generation for Sound, Effective Amortized Probabilistic Inference
Jianlin Li, Leni Ven, Pengyuan Shi, and Yizhou Zhang
(University of Waterloo, Canada)

Publisher's Version Article: popl23main-p354-p (type: Full Paper) doi:10.1145/3571243

Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework
Victor Arrial, Giulio Guerrieri, and Delia Kesner
(Université Paris Cité - CNRS - IRIF, France; Aix Marseille Université - CNRS - LIS, France; Edinburgh Research Centre - Central Software Institute - Huawei, UK; Institut Universitaire de France, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p365-p (type: Full Paper) doi:10.1145/3571244

Fast Coalgebraic Bisimilarity Minimization
Jules Jacobs and Thorsten Wißmann
(Radboud University Nijmegen, Netherlands)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl23main-p373-p (type: Full Paper) doi:10.1145/3571245

An Operational Approach to Library Abstraction under Relaxed Memory Concurrency
Abhishek Kr Singh and Ori Lahav
(Tel Aviv University, Israel)

Publisher's Version Article: popl23main-p380-p (type: Full Paper) doi:10.1145/3571246

Efficient Dual-Numbers Reverse AD via Well-Known Program Transformations
Tom J. Smeding and Matthijs I. L. Vákár
(Utrecht University, Netherlands)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p409-p (type: Full Paper) doi:10.1145/3571247

A Partial Order View of Message-Passing Communication Models
Cinzia Di Giusto, Davide Ferré, Laetitia Laversa, and Etienne Lozes
(Université Côte d'Azur, France; CNRS, France)

Publisher's Version Article: popl23main-p427-p (type: Full Paper) doi:10.1145/3571248

Combining Functional and Automata Synthesis to Discover Causal Reactive Programs
Ria Das, Joshua B. Tenenbaum, Armando Solar-Lezama, and Zenna Tavares
(Stanford University, USA; Massachusetts Institute of Technology, USA; Basis, USA; Columbia University, USA)

Publisher's Version Archive submitted (780 kB) Article: popl23main-p449-p (type: Full Paper) doi:10.1145/3571249

An Order-Theoretic Analysis of Universe Polymorphism
Kuen-Bang Hou (Favonia), Carlo Angiuli, and Reed Mullanix
(University of Minnesota, USA; Carnegie Mellon University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p471-p (type: Full Paper) doi:10.1145/3571250

Statically Resolvable Ambiguity
Viktor Palmkvist, Elias Castegren, Philipp Haller, and David Broman
(KTH Royal Institute of Technology, Sweden; Uppsala University, Sweden)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p477-p (type: Full Paper) doi:10.1145/3571251

The Fine-Grained Complexity of CFL Reachability
Paraschos Koutris and Shaleen Deep
(University of Wisconsin-Madison, USA; Microsoft, USA)

Publisher's Version Article: popl23main-p490-p (type: Full Paper) doi:10.1145/3571252

Taking Back Control in an Intermediate Representation for GPU Computing
Vasileios Klimis, Jack Clark, Alan Baker, David Neto, John Wickerson, and Alastair F. Donaldson
(Imperial College London, UK; Google, Canada; Google, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p511-p (type: Full Paper) doi:10.1145/3571253

Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq
Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, and Steve Zdancewic
(University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP, France; University of Pennsylvania, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p528-p (type: Full Paper) doi:10.1145/3571254

Hefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects
Casper Bach Poulsen and Cas van der Rest
(Delft University of Technology, Netherlands)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p530-p (type: Full Paper) doi:10.1145/3571255

Elements of Quantitative Rewriting
Francesco Gavazzo and Cecilia Di Florio
(University of Pisa, Italy; University of Bologna, Italy)

Publisher's Version Article: popl23main-p531-p (type: Full Paper) doi:10.1145/3571256

Deconstructing the Calculus of Relations with Tape Diagrams
Filippo Bonchi, Alessandro Di Giorgio, and Alessio Santamaria
(University of Pisa, Italy; University of Sussex, UK)

Publisher's Version Article: popl23main-p559-p (type: Full Paper) doi:10.1145/3571257

SSA Translation Is an Abstract Interpretation
Matthieu Lemerre
(Université Paris-Saclay - CEA LIST, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p570-p (type: Full Paper) doi:10.1145/3571258

Probabilistic Resource-Aware Session Types
Ankush Das, Di Wang, and Jan Hoffmann
(Amazon, USA; Carnegie Mellon University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p590-p (type: Full Paper) doi:10.1145/3571259

A Calculus for Amortized Expected Runtimes
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Lena Verscht
(RWTH Aachen University, Germany; Saarland University, Germany; University College London, UK; DTU, Denmark)

Publisher's Version Article: popl23main-p592-p (type: Full Paper) doi:10.1145/3571260

Reconciling Shannon and Scott with a Lattice of Computable Information
Sebastian Hunt, David Sands, and Sandro Stucki
(City University of London, UK; Chalmers University of Technology, Sweden; Amazon Prime Video, Sweden)

Publisher's Version Article: popl23main-p600-p (type: Full Paper) doi:10.1145/3571740

Higher-Order MSL Horn Constraints
Jerome Jochems, Eddie Jones, and Steven Ramsay
(University of Bristol, UK)

Publisher's Version Article: popl23main-p650-p (type: Full Paper) doi:10.1145/3571262

Inductive Synthesis of Structurally Recursive Functional Programs from Non-recursive Expressions
Woosuk Lee and Hangyeol Cho
(Hanyang University, South Korea)

Publisher's Version Published Artifact Archive submitted (710 kB) Artifacts Available Artifacts Reusable Article: popl23main-p658-p (type: Full Paper) doi:10.1145/3571263

Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations
Taro Sekiyama and Hiroshi Unno
(National Institute of Informatics, Japan; University of Tsukuba, Japan; RIKEN AIP, Japan)

Publisher's Version Archive submitted (940 kB) Article: popl23main-p688-p (type: Full Paper) doi:10.1145/3571264

Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification
Hiroshi Unno, Tachio Terauchi, Yu Gu, and Eric Koskinen
(University of Tsukuba, Japan; RIKEN AIP, Japan; Waseda University, Japan; Stevens Institute of Technology, USA)

Publisher's Version Article: popl23main-p691-p (type: Full Paper) doi:10.1145/3571265

Context-Bounded Verification of Context-Free Specifications
Pascal Baumann, Moses Ganardi, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche
(MPI-SWS, Germany)

Publisher's Version Article: popl23main-p699-p (type: Full Paper) doi:10.1145/3571266

Impredicative Observational Equality
Loïc Pujet and Nicolas Tabareau
(Inria, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p756-p (type: Full Paper) doi:10.1145/3571739