POPL – Journal Issue

Constructing Quotient Inductive-Inductive Types
Ambrus Kaposi, András Kovács, and Thorsten Altenkirch
(Eötvös Loránd University, Hungary; University of Nottingham, UK)

Definitional Proof-Irrelevance without K
Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau
(Inria, France; Chalmers University of Technology, Sweden; University of Gothenburg, Sweden; IRIF, France)

Bisimulation as Path Type for Guarded Recursive Types
Rasmus Ejlers Møgelberg and Niccolò Veltri
(IT University of Copenhagen, Denmark)

Abstraction-Safe Effect Handlers via Tunneling
Yizhou Zhang and Andrew C. Myers
(Cornell University, USA)

Abstracting Algebraic Effects
Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski
(University of Wrocław, Poland)

Intersection Types and Runtime Errors in the Pi-Calculus
Ugo Dal Lago, Marc de Visme, Damiano Mazza, and Akira Yoshimizu
(University of Bologna, Italy; Inria, France; University of Lyon, France; ENS Lyon, France; CNRS, France; University of Paris 13, France)

Principality and Approximation under Dimensional Bound
Andrej Dudenhefner and Jakob Rehof
(TU Dortmund, Germany)

Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism with Existentials and Indexed Types
Joshua Dunfield and Neelakantan R. Krishnaswami
(Queen's University, Canada; University of Cambridge, UK)

Fully Abstract Module Compilation
Karl Crary
(Carnegie Mellon University, USA)

Polymorphic Symmetric Multiple Dispatch with Variance
Gyunghee Park, Jaemin Hong, Guy L. Steele Jr., and Sukyoung Ryu
(KAIST, South Korea; Oracle Labs, USA)

Abstracting Extensible Data Types: Or, Rows by Any Other Name
J. Garrett Morris and James McKinna
(University of Kansas, USA; University of Edinburgh, UK)

Type-Guided Worst-Case Input Generation
Di Wang and Jan Hoffmann
(Carnegie Mellon University, USA)

Live Functional Programming with Typed Holes
Cyrus Omar, Ian Voysey, Ravi Chugh, and Matthew A. Hammer
(University of Chicago, USA; Carnegie Mellon University, USA; University of Colorado Boulder, USA)

Gradual Type Theory
Max S. New, Daniel R. Licata, and Amal Ahmed
(Northeastern University, USA; Wesleyan University, USA; Inria, France)

Gradual Typing: A New Perspective
Giuseppe Castagna, Victor Lanvin, Tommaso Petrucciani, and Jeremy G. Siek
(CNRS, France; University of Paris Diderot, France; University of Genoa, Italy; Indiana University, USA)

Gradual Parametricity, Revisited
Matías Toro, Elizabeth Labrada, and Éric Tanter
(University of Chile, Chile; Inria, France)

Dynamic Type Inference for Gradual Hindley–Milner Typing
Yusuke Miyazaki, Taro Sekiyama, and Atsushi Igarashi
(Kyoto University, Japan; National Institute of Informatics, Japan)

StkTokens: Enforcing Well-Bracketed Control Flow and Stack Encapsulation Using Linear Capabilities
Lau Skorstengaard, Dominique Devriese, and Lars Birkedal
(Aarhus University, Denmark; Vrije Universiteit Brussel, Belgium)

Modalities, Cohesion, and Information Flow
G. A. Kavvos
(Wesleyan University, USA)

Familial Monads and Structural Operational Semantics
Tom Hirschowitz
(Grenoble Alps University, France; Savoie Mont Blanc University, France; CNRS, France; LAMA, France)

Bindings as Bounded Natural Functors
Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, and Dmitriy Traytel
(Vrije Universiteit Amsterdam, Netherlands; Max Planck Institute for Informatics, Germany; Middlesex University, UK; Institute of Mathematics at Romanian Academy, Romania; ETH Zurich, Switzerland)

Categorical Combinatorics of Scheduling and Synchronization in Game Semantics
Paul-André Mellies
(CNRS, France; University of Paris Diderot, France)

Better Late Than Never: A Fully-Abstract Semantics for Classical Processes
Wen Kokke, Fabrizio Montesi, and Marco Peressotti
(University of Edinburgh, UK; University of Southern Denmark, Denmark)

Diagrammatic Algebra: From Linear to Concurrent Systems
Filippo Bonchi, Joshua Holland, Robin Piedeleu, Paweł Sobociński, and Fabio Zanasi
(University of Pisa, Italy; University of Southampton, UK; University of Oxford, UK; University College London, UK)

Fixpoint Games on Continuous Lattices
Paolo Baldan, Barbara König, Christina Mika-Michalski, and Tommaso Padoan
(University of Padua, Italy; University of Duisburg-Essen, Germany)

Two Sides of the Same Coin: Session Types and Game Semantics: A Synchronous Side and an Asynchronous Side
Simon Castellan and Nobuko Yoshida
(Imperial College London, UK)

Exceptional Asynchronous Session Types: Session Types without Tiers
Simon Fowler, Sam Lindley, J. Garrett Morris, and Sára Decova
(University of Edinburgh, UK; University of Kansas, USA)

Distributed Programming using Role-Parametric Session Types in Go: Statically-Typed Endpoint APIs for Dynamically-Instantiated Communication Structures
David Castro, Raymond Hu, Sung-Shik Jongmans, Nicholas Ng, and Nobuko Yoshida
(Imperial College London, UK; Open University of the Netherlands, Netherlands)

Less Is More: Multiparty Session Types Revisited
Alceste Scalas and Nobuko Yoshida
(Imperial College London, UK)

Quantitative Robustness Analysis of Quantum Programs
Shih-Han Hung, Kesha Hietala, Shaopeng Zhu, Mingsheng Ying, Michael Hicks, and Xiaodi Wu
(University of Maryland, USA; University of Technology Sydney, Australia; Institute of Software at Chinese Academy of Sciences, China; Tsinghua University, China)

Game Semantics for Quantum Programming
Pierre Clairambault, Marc De Visme, and Glynn Winskel
(University of Lyon, France; CNRS, France; ENS Lyon, France; University of Cambridge, UK)

Quantum Relational Hoare Logic
Dominique Unruh
(University of Tartu, Estonia)

Quantitative Separation Logic: A Logic for Reasoning about Probabilistic Pointer Programs
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll
(RWTH Aachen University, Germany)

Probabilistic Programming with Densities in SlicStan: Efficient, Flexible, and Deterministic
Maria I. Gorinova, Andrew D. Gordon, and Charles Sutton
(University of Edinburgh, UK; Microsoft Research, UK; Google Brain, USA)

A Domain Theory for Statistical Probabilistic Programming
Matthijs Vákár, Ohad Kammar, and Sam Staton
(Columbia University, USA; University of Oxford, UK)

Bayesian Synthesis of Probabilistic Programs for Automatic Data Modeling
Feras A. Saad, Marco F. Cusumano-Towner, Ulrich Schaechtle, Martin C. Rinard, and Vikash K. Mansinghka
(Massachusetts Institute of Technology, USA)

Formal Verification of Higher-Order Probabilistic Programs: Reasoning about Approximation, Convergence, Bayesian Inference, and Optimization
Tetsuya Sato, Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Justin Hsu
(SUNY Buffalo, USA; IMDEA Software Institute, Spain; MPI-SWS, Germany; University of Wisconsin-Madison, USA)

Trace Abstraction Modulo Probability
Calvin Smith, Justin Hsu, and Aws Albarghouthi
(University of Wisconsin-Madison, USA)

code2vec: Learning Distributed Representations of Code
Uri Alon, Meital Zilberstein, Omer Levy, and Eran Yahav
(Technion, Israel; Facebook AI Research, USA)

An Abstract Domain for Certifying Neural Networks
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev
(ETH Zurich, Switzerland)

A²I: Abstract² Interpretation
Patrick Cousot, Roberto Giacobazzi, and Francesco Ranzato
(New York University, USA; University of Verona, Italy; IMDEA Software Institute, Spain; University of Padua, Italy)

Concerto: A Framework for Combined Concrete and Abstract Interpretation
John Toman and Dan Grossman
(University of Washington, USA)

Skeletal Semantics and Their Interpretations
Martin Bodin, Philippa Gardner, Thomas Jensen, and Alan Schmitt
(Imperial College London, UK; Inria, France)

Refinement of Path Expressions for Static Analysis
John Cyphert, Jason Breck, Zachary Kincaid, and Thomas Reps
(University of Wisconsin, USA; Princeton University, USA; GrammaTech, USA)

Decidable Verification of Uninterpreted Programs
Umang Mathur, P. Madhusudan, and Mahesh Viswanathan
(University of Illinois at Urbana-Champaign, USA)

Inferring Frame Conditions with Static Correlation Analysis
Oana F. Andreescu, Thomas Jensen, Stéphane Lescuyer, and Benoît Montagu
(Internet of Trust, France; Inria, France; Prove & Run, France)

Context-, Flow-, and Field-Sensitive Data-Flow Analysis using Synchronized Pushdown Systems
Johannes Späth, Karim Ali, and Eric Bodden
(Fraunhofer IEM, Germany; University of Alberta, Canada; University of Paderborn, Germany)

Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations
Taolue Chen, Matthew Hague, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu
(Birkbeck University of London, UK; Royal Holloway University of London, UK; University of Oxford, UK; Uppsala University, Sweden; Institute of Software at Chinese Academy of Sciences, China)

Modular Quantitative Monitoring
Rajeev Alur, Konstantinos Mamouras, and Caleb Stanford
(University of Pennsylvania, USA; Rice University, USA)

Bounded Model Checking of Signal Temporal Logic Properties using Syntactic Separation
Kyungmin Bae and Jia Lee
(POSTECH, South Korea)

Adventures in Monitorability: From Branching to Linear Time and Back Again
Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen
(Gran Sasso Science Institute, Iceland; Reykjavik University, Iceland; University of Malta, Malta; University of Kiel, Germany; University of Liverpool, UK)

Efficient Parameterized Algorithms for Data Packing
Krishnendu Chatterjee, Amir Kafshdar Goharshady, Nastaran Okati, and Andreas Pavlogiannis
(IST Austria, Austria; Ferdowsi University of Mashhad, Iran; EPFL, Switzerland)

Fast and Exact Analysis for LRU Caches
Valentin Touzeau, Claire Maïza, David Monniaux, and Jan Reineke
(Grenoble Alps University, France; Grenoble INP, France; CNRS, France; Saarland University, Germany)

Closed Forms for Numerical Loops
Zachary Kincaid, Jason Breck, John Cyphert, and Thomas Reps
(Princeton University, USA; University of Wisconsin, USA; GrammaTech, USA)

Efficient Automated Repair of High Floating-Point Errors in Numerical Libraries
Xin Yi, Liqian Chen, Xiaoguang Mao, and Tao Ji
(National University of Defense Technology, China)

A True Positives Theorem for a Static Race Detector
Nikos Gorogiannis, Peter W. O'Hearn, and Ilya Sergey
(Facebook, UK; Middlesex University, UK; University College London, UK; Yale-NUS College, Singapore; National University of Singapore, Singapore)

Decoupling Lock-Free Data Structures from Memory Reclamation for Static Analysis
Roland Meyer and Sebastian Wolff
(TU Braunschweig, Germany)

Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs
Klaus v. Gleissenthall, Rami Gökhan Kıcı, Alexander Bakst, Deian Stefan, and Ranjit Jhala
(University of California at San Diego, USA)

Weak-Consistency Specification via Visibility Relaxation
Michael Emmi and Constantin Enea
(SRI International, USA; IRIF, France; University of Paris Diderot, France; CNRS, France)

A Calculus for Esterel: If can, can. If no can, no can.
Spencer P. Florence, Shu-Hung You, Jesse A. Tov, and Robert Bruce Findler
(Northwestern University, USA)

An Abstract Stack Based Approach to Verified Compositional Compilation to Machine Code
Yuting Wang, Pierre Wilke, and Zhong Shao
(Yale University, USA; CentraleSupélec, France)

A Verified, Efficient Embedding of a Verifiable Assembly Language
Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi, and Nikhil Swamy
(Carnegie Mellon University, USA; Princeton University, USA; Microsoft Research, USA; Microsoft Research, India)

A Separation Logic for Concurrent Randomized Programs
Joseph Tassarotti and Robert Harper
(Carnegie Mellon University, USA)

Iron: Managing Obligations in Higher-Order Concurrent Separation Logic
Aleš Bizjak, Daniel Gratzer, Robbert Krebbers, and Lars Birkedal
(Aarhus University, Denmark; Delft University of Technology, Netherlands)

JaVerT 2.0: Compositional Symbolic Execution for JavaScript
José Fragoso Santos, Petar Maksimović, Gabriela Sampaio, and Philippa Gardner
(Imperial College London, UK; Mathematical Institute SASA, Serbia)

Exploring C Semantics and Pointer Provenance
Kayvan Memarian, Victor B. F. Gomes, Brooks Davis, Stephen Kell, Alexander Richardson, Robert N. M. Watson, and Peter Sewell
(University of Cambridge, UK; SRI International, USA)

On Library Correctness under Weak Memory Consistency: Specifying and Verifying Concurrent Libraries under Declarative Consistency Models
Azalea Raad, Marko Doko, Lovro Rožić, Ori Lahav, and Viktor Vafeiadis
(MPI-SWS, Germany; Tel Aviv University, Israel)

Bridging the Gap between Programming Languages and Hardware Weak Memory Models
Anton Podkopaev, Ori Lahav, and Viktor Vafeiadis
(St. Petersburg University, Russia; JetBrains Research, Russia; MPI-SWS, Germany; Tel Aviv University, Israel)

Grounding Thin-Air Reads with Event Structures
Soham Chakraborty and Viktor Vafeiadis
(MPI-SWS, Germany)

ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and Peter Sewell
(University of Cambridge, UK; University of Edinburgh, UK; ARM, UK; SRI International, USA)

Structuring the Synthesis of Heap-Manipulating Programs
Nadia Polikarpova and Ilya Sergey
(University of California at San Diego, USA; Yale-NUS College, Singapore; National University of Singapore, Singapore)

FrAngel: Component-Based Synthesis with Control Structures
Kensen Shi, Jacob Steinhardt, and Percy Liang
(Stanford University, USA)

Hamsaz: Replication Coordination Analysis and Synthesis
Farzin Houshmand and Mohsen Lesani
(University of California at Riverside, USA)

LWeb: Information Flow Security for Multi-tier Web Applications
James Parker, Niki Vazou, and Michael Hicks
(University of Maryland, USA; IMDEA Software Institute, Spain)

From Fine- to Coarse-Grained Dynamic Information Flow Control and Back
Marco Vassena, Alejandro Russo, Deepak Garg, Vineet Rajani, and Deian Stefan
(Chalmers University of Technology, Sweden; MPI-SWS, Germany; University of California at San Diego, USA)

CT-Wasm: Type-Driven Secure Cryptography for the Web Ecosystem
Conrad Watt, John Renner, Natalie Popescu, Sunjay Cauligi, and Deian Stefan
(University of Cambridge, UK; University of California at San Diego, USA)