| |
Aiken, Alex
|
Proc. ACM Program. Lang., vol. 6, issue POPL: "Induction Duality: Primal-Dual ..."
Induction Duality: Primal-Dual Search for Invariants
Oded Padon, James R. Wilcox, Jason R. Koenig, Kenneth L. McMillan, and Alex Aiken
(VMware Research, USA; Stanford University, USA; Certora, USA; University of Texas at Austin, USA)
 Publisher's Version
 Published Artifact
Artifacts Available
Artifacts Functional
Article: popl22main-p428-p doi:10.1145/3498712
|
| |
Albarghouthi, Aws |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Interval Universal Approximation ..."
Interval Universal Approximation for Neural Networks
Zi Wang, Aws Albarghouthi, Gautam Prakriya, and Somesh Jha
(University of Wisconsin-Madison, USA; Chinese University of Hong Kong, China; University of Wisconsin, USA)
Publisher's Version
Archive submitted (830 kB)
Article: popl22main-p61-p doi:10.1145/3498675
|
| |
Amin, Nada |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Reasoning about “Reasoning ..."
Reasoning about “Reasoning about Reasoning”: Semantics and Contextual Equivalence for Probabilistic Programs with Nested Queries and Recursion
Yizhou Zhang and Nada Amin
(University of Waterloo, Canada; Harvard University, USA)
Publisher's Version
Article: popl22main-p66-p doi:10.1145/3498677
|
| |
Balzer, Stephanie
|
Proc. ACM Program. Lang., vol. 6, issue POPL: "Connectivity Graphs: A Method ..."
Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation Logic
Jules Jacobs, Stephanie Balzer, and Robbert Krebbers
(Radboud University Nijmegen, Netherlands; Carnegie Mellon University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p6-p doi:10.1145/3498662
|
| |
Bao, Jialu |
Proc. ACM Program. Lang., vol. 6, issue POPL: "A Separation Logic for Negative ..."
A Separation Logic for Negative Dependence
Jialu Bao, Marco Gaboardi, Justin Hsu, and Joseph Tassarotti
(Cornell University, USA; Boston University, USA; Boston College, USA)
Publisher's Version
Article: popl22main-p550-p doi:10.1145/3498719
|
| |
Batty, Mark |
Proc. ACM Program. Lang., vol. 6, issue POPL: "The Leaky Semicolon: Compositional ..."
The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Concurrency
Alan Jeffrey, James Riely, Mark Batty, Simon Cooksey, Ilya Kaysin, and Anton Podkopaev
(Roblox, USA; DePaul University, USA; University of Kent, UK; JetBrains Research, Russia; University of Cambridge, UK; HSE University, Russia)
Publisher's Version
Published Artifact
Artifacts Available
Article: popl22main-p459-p doi:10.1145/3498716
|
| |
Baumann, Pascal |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Context-Bounded Verification ..."
Context-Bounded Verification of Thread Pools
Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche
(MPI-SWS, Germany)
Publisher's Version
Article: popl22main-p90-p doi:10.1145/3498678
|
| |
Berdine, Josh |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Concurrent Incorrectness Separation ..."
Concurrent Incorrectness Separation Logic
Azalea Raad, Josh Berdine, Derek Dreyer, and Peter W. O'Hearn
(Imperial College London, UK; Meta, UK; MPI-SWS, Germany; University College London, UK)
Publisher's Version
Article: popl22main-p233-p doi:10.1145/3498695
|
| |
Bernstein, Gilbert Louis |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Verified Tensor-Program Optimization ..."
Verified Tensor-Program Optimization Via High-Level Scheduling Rewrites
Amanda Liu, Gilbert Louis Bernstein, Adam Chlipala, and Jonathan Ragan-Kelley
(Massachusetts Institute of Technology, USA; University of California at Berkeley, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p523-p doi:10.1145/3498717
|
| |
Blanvillain, Olivier |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Type-Level Programming with ..."
Type-Level Programming with Match Types
Olivier Blanvillain, Jonathan Immanuel Brachthäuser, Maxime Kjaer, and Martin Odersky
(EPFL, Switzerland; University of Tübingen, Germany)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p258-p doi:10.1145/3498698
|
| |
Brachthäuser, Jonathan Immanuel |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Type-Level Programming with ..."
Type-Level Programming with Match Types
Olivier Blanvillain, Jonathan Immanuel Brachthäuser, Maxime Kjaer, and Martin Odersky
(EPFL, Switzerland; University of Tübingen, Germany)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p258-p doi:10.1145/3498698
|
| |
Brendel, Ana |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Bottom-Up Synthesis of Recursive ..."
Bottom-Up Synthesis of Recursive Functional Programs using Angelic Execution
Anders Miltner, Adrian Trejo Nuñez, Ana Brendel, Swarat Chaudhuri, and Isil Dillig
(University of Texas at Austin, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p124-p doi:10.1145/3498682
|
| |
Campbell, Eric Hayden
|
Proc. ACM Program. Lang., vol. 6, issue POPL: "Dependently-Typed Data Plane ..."
Dependently-Typed Data Plane Programming
Matthias Eichholz, Eric Hayden Campbell, Matthias Krebs, Nate Foster, and Mira Mezini
(TU Darmstadt, Germany; Cornell University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Article: popl22main-p311-p doi:10.1145/3498701
|
| |
Campion, Marco |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Partial (In)Completeness in ..."
Partial (In)Completeness in Abstract Interpretation: Limiting the Imprecision in Program Analysis
Marco Campion, Mila Dalla Preda, and Roberto Giacobazzi
(University of Verona, Italy)
Publisher's Version
Article: popl22main-p597-p doi:10.1145/3498721
|
| |
Carbin, Michael |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Twist: Sound Reasoning for ..."
Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs
Charles Yuan, Christopher McNally, and Michael Carbin
(Massachusetts Institute of Technology, USA)
Publisher's Version
Published Artifact
Archive submitted (690 kB)
Artifacts Available
Artifacts Reusable
Article: popl22main-p167-p doi:10.1145/3498691
|
| |
Castagna, Giuseppe |
Proc. ACM Program. Lang., vol. 6, issue POPL: "On Type-Cases, Union Elimination, ..."
On Type-Cases, Union Elimination, and Occurrence Typing
Giuseppe Castagna, Mickaël Laurent, Kim Nguyễn, and Matthew Lutze
(CNRS, France; Université de Paris, France; Université Paris-Saclay, France)
Publisher's Version
Published Artifact
Archive submitted (1.1 MB)
Artifacts Available
Artifacts Reusable
Article: popl22main-p58-p doi:10.1145/3498674
|
| |
Chaudhuri, Swarat |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Bottom-Up Synthesis of Recursive ..."
Bottom-Up Synthesis of Recursive Functional Programs using Angelic Execution
Anders Miltner, Adrian Trejo Nuñez, Ana Brendel, Swarat Chaudhuri, and Isil Dillig
(University of Texas at Austin, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p124-p doi:10.1145/3498682
|
| |
Chen, Taolue |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Solving String Constraints ..."
Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables
Taolue Chen, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu
(Birkbeck University of London, UK; Royal Holloway University of London, UK; Tsinghua University, China; Institute of Software at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; TU Kaiserslautern, Germany; MPI-SWS, Germany; Uppsala University, Sweden)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p350-p doi:10.1145/3498707
|
| |
Chistikov, Dmitry |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Subcubic Certificates for ..."
Subcubic Certificates for CFL Reachability
Dmitry Chistikov, Rupak Majumdar, and Philipp Schepper
(University of Warwick, UK; MPI-SWS, Germany; CISPA, Germany)
Publisher's Version
Article: popl22main-p322-p doi:10.1145/3498702
|
| |
Chlipala, Adam |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Certifying Derivation of State ..."
Certifying Derivation of State Machines from Coroutines
Mirai Ikebuchi, Andres Erbsen, and Adam Chlipala
(National Institute of Informatics, Japan; Massachusetts Institute of Technology, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p137-p doi:10.1145/3498685
Proc. ACM Program. Lang., vol. 6, issue POPL: "Verified Tensor-Program Optimization ..."
Verified Tensor-Program Optimization Via High-Level Scheduling Rewrites
Amanda Liu, Gilbert Louis Bernstein, Adam Chlipala, and Jonathan Ragan-Kelley
(Massachusetts Institute of Technology, USA; University of California at Berkeley, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p523-p doi:10.1145/3498717
|
| |
Choudhury, Vikraman |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Symmetries in Reversible Programming: ..."
Symmetries in Reversible Programming: From Symmetric Rig Groupoids to Reversible Programming Languages
Vikraman Choudhury, Jacek Karwowski, and Amr Sabry
(Indiana University, USA; University of Cambridge, UK; University of Warsaw, Poland)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p31-p doi:10.1145/3498667
|
| |
Ciccone, Luca |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Fair Termination of Binary ..."
Fair Termination of Binary Sessions
Luca Ciccone and Luca Padovani
(University of Turin, Italy)
Publisher's Version
Published Artifact
Archive submitted (600 kB)
Artifacts Available
Artifacts Reusable
Article: popl22main-p30-p doi:10.1145/3498666
|
| |
Cooksey, Simon |
Proc. ACM Program. Lang., vol. 6, issue POPL: "The Leaky Semicolon: Compositional ..."
The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Concurrency
Alan Jeffrey, James Riely, Mark Batty, Simon Cooksey, Ilya Kaysin, and Anton Podkopaev
(Roblox, USA; DePaul University, USA; University of Kent, UK; JetBrains Research, Russia; University of Cambridge, UK; HSE University, Russia)
Publisher's Version
Published Artifact
Artifacts Available
Article: popl22main-p459-p doi:10.1145/3498716
|
| |
Dal Lago, Ugo
|
Proc. ACM Program. Lang., vol. 6, issue POPL: "Effectful Program Distancing ..."
Effectful Program Distancing
Ugo Dal Lago and Francesco Gavazzo
(University of Bologna, Italy; Inria, France)
Publisher's Version
Article: popl22main-p94-p doi:10.1145/3498680
Proc. ACM Program. Lang., vol. 6, issue POPL: "A Relational Theory of Effects ..."
A Relational Theory of Effects and Coeffects
Ugo Dal Lago and Francesco Gavazzo
(University of Bologna, Italy; Inria, France)
Publisher's Version
Article: popl22main-p168-p doi:10.1145/3498692
|
| |
Dalla Preda, Mila |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Partial (In)Completeness in ..."
Partial (In)Completeness in Abstract Interpretation: Limiting the Imprecision in Program Analysis
Marco Campion, Mila Dalla Preda, and Roberto Giacobazzi
(University of Verona, Italy)
Publisher's Version
Article: popl22main-p597-p doi:10.1145/3498721
|
| |
Dang, Hoang-Hai |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Simuliris: A Separation Logic ..."
Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations
Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, and Derek Dreyer
(MPI-SWS, Germany; Radboud University Nijmegen, Netherlands; KAIST, South Korea)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p158-p doi:10.1145/3498689
|
| |
De Amorim, Arthur Azevedo |
Proc. ACM Program. Lang., vol. 6, issue POPL: "On Incorrectness Logic and ..."
On Incorrectness Logic and Kleene Algebra with Top and Tests
Cheng Zhang, Arthur Azevedo de Amorim, and Marco Gaboardi
(Boston University, USA)
Publisher's Version
Article: popl22main-p160-p doi:10.1145/3498690
|
| |
Delaware, Benjamin |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Oblivious Algebraic Data Types ..."
Oblivious Algebraic Data Types
Qianchuan Ye and Benjamin Delaware
(Purdue University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p429-p doi:10.1145/3498713
|
| |
Dillig, Isil |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Bottom-Up Synthesis of Recursive ..."
Bottom-Up Synthesis of Recursive Functional Programs using Angelic Execution
Anders Miltner, Adrian Trejo Nuñez, Ana Brendel, Swarat Chaudhuri, and Isil Dillig
(University of Texas at Austin, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p124-p doi:10.1145/3498682
Proc. ACM Program. Lang., vol. 6, issue POPL: "SolType: Refinement Types ..."
SolType: Refinement Types for Arithmetic Overflow in Solidity
Bryan Tan, Benjamin Mariano, Shuvendu K. Lahiri, Isil Dillig, and Yu Feng
(University of California at Santa Barbara, USA; University of Texas at Austin, USA; Microsoft Research, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p27-p doi:10.1145/3498665
|
| |
Dreyer, Derek |
Proc. ACM Program. Lang., vol. 6, issue POPL: "VIP: Verifying Real-World ..."
VIP: Verifying Real-World C Idioms with Integer-Pointer Casts
Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, and Peter Sewell
(MPI-SWS, Germany; University of Cambridge, UK; Radboud University Nijmegen, Netherlands)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p95-p doi:10.1145/3498681
Proc. ACM Program. Lang., vol. 6, issue POPL: "Simuliris: A Separation Logic ..."
Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations
Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, and Derek Dreyer
(MPI-SWS, Germany; Radboud University Nijmegen, Netherlands; KAIST, South Korea)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p158-p doi:10.1145/3498689
Proc. ACM Program. Lang., vol. 6, issue POPL: "Concurrent Incorrectness Separation ..."
Concurrent Incorrectness Separation Logic
Azalea Raad, Josh Berdine, Derek Dreyer, and Peter W. O'Hearn
(Imperial College London, UK; Meta, UK; MPI-SWS, Germany; University College London, UK)
Publisher's Version
Article: popl22main-p233-p doi:10.1145/3498695
|
| |
Eichholz, Matthias
|
Proc. ACM Program. Lang., vol. 6, issue POPL: "Dependently-Typed Data Plane ..."
Dependently-Typed Data Plane Programming
Matthias Eichholz, Eric Hayden Campbell, Matthias Krebs, Nate Foster, and Mira Mezini
(TU Darmstadt, Germany; Cornell University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Article: popl22main-p311-p doi:10.1145/3498701
|
| |
Eisenberg, Richard A. |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Provably Correct, Asymptotically ..."
Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic Differentiation
Faustyna Krawiec, Simon Peyton Jones, Neel Krishnaswami, Tom Ellis, Richard A. Eisenberg, and Andrew Fitzgibbon
(University of Cambridge, UK; Microsoft Research, UK; Tweag, France)
Publisher's Version
Article: popl22main-p397-p doi:10.1145/3498710
|
| |
Ellis, Tom |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Provably Correct, Asymptotically ..."
Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic Differentiation
Faustyna Krawiec, Simon Peyton Jones, Neel Krishnaswami, Tom Ellis, Richard A. Eisenberg, and Andrew Fitzgibbon
(University of Cambridge, UK; Microsoft Research, UK; Tweag, France)
Publisher's Version
Article: popl22main-p397-p doi:10.1145/3498710
|
| |
Erbsen, Andres |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Certifying Derivation of State ..."
Certifying Derivation of State Machines from Coroutines
Mirai Ikebuchi, Andres Erbsen, and Adam Chlipala
(National Institute of Informatics, Japan; Massachusetts Institute of Technology, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p137-p doi:10.1145/3498685
|
| |
Feldman, Yotam M. Y.
|
Proc. ACM Program. Lang., vol. 6, issue POPL: "Property-Directed Reachability ..."
Property-Directed Reachability as Abstract Interpretation in the Monotone Theory
Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, and James R. Wilcox
(Tel Aviv University, Israel; Certora, USA)
Publisher's Version
Article: popl22main-p65-p doi:10.1145/3498676
|
| |
Feng, Yu |
Proc. ACM Program. Lang., vol. 6, issue POPL: "SolType: Refinement Types ..."
SolType: Refinement Types for Arithmetic Overflow in Solidity
Bryan Tan, Benjamin Mariano, Shuvendu K. Lahiri, Isil Dillig, and Yu Feng
(University of California at Santa Barbara, USA; University of Texas at Austin, USA; Microsoft Research, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p27-p doi:10.1145/3498665
|
| |
Fiore, Marcelo |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Formal Metatheory of Second-Order ..."
Formal Metatheory of Second-Order Abstract Syntax
Marcelo Fiore and Dmitrij Szamozvancev
(University of Cambridge, UK)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p437-p doi:10.1145/3498715
|
| |
Fitzgibbon, Andrew |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Provably Correct, Asymptotically ..."
Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic Differentiation
Faustyna Krawiec, Simon Peyton Jones, Neel Krishnaswami, Tom Ellis, Richard A. Eisenberg, and Andrew Fitzgibbon
(University of Cambridge, UK; Microsoft Research, UK; Tweag, France)
Publisher's Version
Article: popl22main-p397-p doi:10.1145/3498710
|
| |
Flores-Lamas, Alejandro |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Solving String Constraints ..."
Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables
Taolue Chen, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu
(Birkbeck University of London, UK; Royal Holloway University of London, UK; Tsinghua University, China; Institute of Software at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; TU Kaiserslautern, Germany; MPI-SWS, Germany; Uppsala University, Sweden)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p350-p doi:10.1145/3498707
|
| |
Foster, Nate |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Dependently-Typed Data Plane ..."
Dependently-Typed Data Plane Programming
Matthias Eichholz, Eric Hayden Campbell, Matthias Krebs, Nate Foster, and Mira Mezini
(TU Darmstadt, Germany; Cornell University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Article: popl22main-p311-p doi:10.1145/3498701
|
| |
Gaboardi, Marco
|
Proc. ACM Program. Lang., vol. 6, issue POPL: "On Incorrectness Logic and ..."
On Incorrectness Logic and Kleene Algebra with Top and Tests
Cheng Zhang, Arthur Azevedo de Amorim, and Marco Gaboardi
(Boston University, USA)
Publisher's Version
Article: popl22main-p160-p doi:10.1145/3498690
Proc. ACM Program. Lang., vol. 6, issue POPL: "A Separation Logic for Negative ..."
A Separation Logic for Negative Dependence
Jialu Bao, Marco Gaboardi, Justin Hsu, and Joseph Tassarotti
(Cornell University, USA; Boston University, USA; Boston College, USA)
Publisher's Version
Article: popl22main-p550-p doi:10.1145/3498719
|
| |
Gäher, Lennard |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Simuliris: A Separation Logic ..."
Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations
Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, and Derek Dreyer
(MPI-SWS, Germany; Radboud University Nijmegen, Netherlands; KAIST, South Korea)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p158-p doi:10.1145/3498689
|
| |
Garg, Deepak |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Pirouette: Higher-Order Typed ..."
Pirouette: Higher-Order Typed Functional Choreographies
Andrew K. Hirsch and Deepak Garg
(MPI-SWS, Germany)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p131-p doi:10.1145/3498684
Proc. ACM Program. Lang., vol. 6, issue POPL: "Isolation without Taxation: ..."
Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFI
Matthew Kolosick, Shravan Narayan, Evan Johnson, Conrad Watt, Michael LeMay, Deepak Garg, Ranjit Jhala, and Deian Stefan
(University of California at San Diego, USA; University of Cambridge, UK; Intel Labs, USA; MPI-SWS, Germany)
Publisher's Version
Article: popl22main-p151-p doi:10.1145/3498688
|
| |
Gavazzo, Francesco |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Effectful Program Distancing ..."
Effectful Program Distancing
Ugo Dal Lago and Francesco Gavazzo
(University of Bologna, Italy; Inria, France)
Publisher's Version
Article: popl22main-p94-p doi:10.1145/3498680
Proc. ACM Program. Lang., vol. 6, issue POPL: "A Relational Theory of Effects ..."
A Relational Theory of Effects and Coeffects
Ugo Dal Lago and Francesco Gavazzo
(University of Bologna, Italy; Inria, France)
Publisher's Version
Article: popl22main-p168-p doi:10.1145/3498692
|
| |
Gélineau, Samuel |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Mœbius: Metaprogramming using ..."
Mœbius: Metaprogramming using Contextual Types: The Stage Where System F Can Pattern Match on Itself
Junyoung Jang, Samuel Gélineau, Stefan Monnier, and Brigitte Pientka
(McGill University, Canada; SimSpace, Canada; Université de Montréal, Canada)
Publisher's Version
Article: popl22main-p294-p doi:10.1145/3498700
|
| |
Giacobazzi, Roberto |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Partial (In)Completeness in ..."
Partial (In)Completeness in Abstract Interpretation: Limiting the Imprecision in Program Analysis
Marco Campion, Mila Dalla Preda, and Roberto Giacobazzi
(University of Verona, Italy)
Publisher's Version
Article: popl22main-p597-p doi:10.1145/3498721
|
| |
Gladstein, Vladimir |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Truly Stateless, Optimal Dynamic ..."
Truly Stateless, Optimal Dynamic Partial Order Reduction
Michalis Kokologiannakis, Iason Marmanis, Vladimir Gladstein, and Viktor Vafeiadis
(MPI-SWS, Germany; St. Petersburg University, Russia; JetBrains Research, Russia)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p424-p doi:10.1145/3498711
|
| |
Grodin, Harrison |
Proc. ACM Program. Lang., vol. 6, issue POPL: "A Cost-Aware Logical Framework ..."
A Cost-Aware Logical Framework
Yue Niu, Jonathan Sterling, Harrison Grodin, and Robert Harper
(Carnegie Mellon University, USA; Aarhus University, Denmark)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p47-p doi:10.1145/3498670
|
| |
Gurfinkel, Arie |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Solving Constrained Horn Clauses ..."
Solving Constrained Horn Clauses Modulo Algebraic Data Types and Recursive Functions
Hari Govind V K, Sharon Shoham, and Arie Gurfinkel
(University of Waterloo, Canada; Tel Aviv University, Israel)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p629-p doi:10.1145/3498722
|
| |
Hague, Matthew
|
Proc. ACM Program. Lang., vol. 6, issue POPL: "Solving String Constraints ..."
Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables
Taolue Chen, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu
(Birkbeck University of London, UK; Royal Holloway University of London, UK; Tsinghua University, China; Institute of Software at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; TU Kaiserslautern, Germany; MPI-SWS, Germany; Uppsala University, Sweden)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p350-p doi:10.1145/3498707
|
| |
Han, Zhilei |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Solving String Constraints ..."
Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables
Taolue Chen, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu
(Birkbeck University of London, UK; Royal Holloway University of London, UK; Tsinghua University, China; Institute of Software at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; TU Kaiserslautern, Germany; MPI-SWS, Germany; Uppsala University, Sweden)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p350-p doi:10.1145/3498707
|
| |
Harper, Robert |
Proc. ACM Program. Lang., vol. 6, issue POPL: "A Cost-Aware Logical Framework ..."
A Cost-Aware Logical Framework
Yue Niu, Jonathan Sterling, Harrison Grodin, and Robert Harper
(Carnegie Mellon University, USA; Aarhus University, Denmark)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p47-p doi:10.1145/3498670
|
| |
He, Wenlei |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Profile Inference Revisited ..."
Profile Inference Revisited
Wenlei He, Julián Mestre, Sergey Pupyrev, Lei Wang, and Hongtao Yu
(Facebook, USA; University of Sydney, Australia)
Publisher's Version
Article: popl22main-p431-p doi:10.1145/3498714
|
| |
Heunen, Chris |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Quantum Information Effects ..."
Quantum Information Effects
Chris Heunen and Robin Kaarsgaard
(University of Edinburgh, UK)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p9-p doi:10.1145/3498663
|
| |
Hirsch, Andrew K. |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Pirouette: Higher-Order Typed ..."
Pirouette: Higher-Order Typed Functional Choreographies
Andrew K. Hirsch and Deepak Garg
(MPI-SWS, Germany)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p131-p doi:10.1145/3498684
|
| |
Hou (Favonia), Kuen-Bang |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Logarithm and Program Testing ..."
Logarithm and Program Testing
Kuen-Bang Hou (Favonia) and Zhuyang Wang
(University of Minnesota, USA)
Publisher's Version
Published Artifact
Archive submitted (540 kB)
Artifacts Available
Artifacts Reusable
Article: popl22main-p764-p doi:10.1145/3498726
|
| |
Hsu, Justin |
Proc. ACM Program. Lang., vol. 6, issue POPL: "A Separation Logic for Negative ..."
A Separation Logic for Negative Dependence
Jialu Bao, Marco Gaboardi, Justin Hsu, and Joseph Tassarotti
(Cornell University, USA; Boston University, USA; Boston College, USA)
Publisher's Version
Article: popl22main-p550-p doi:10.1145/3498719
|
| |
Hu, Denghang |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Solving String Constraints ..."
Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables
Taolue Chen, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu
(Birkbeck University of London, UK; Royal Holloway University of London, UK; Tsinghua University, China; Institute of Software at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; TU Kaiserslautern, Germany; MPI-SWS, Germany; Uppsala University, Sweden)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p350-p doi:10.1145/3498707
|
| |
Ikebuchi, Mirai
|
Proc. ACM Program. Lang., vol. 6, issue POPL: "Certifying Derivation of State ..."
Certifying Derivation of State Machines from Coroutines
Mirai Ikebuchi, Andres Erbsen, and Adam Chlipala
(National Institute of Informatics, Japan; Massachusetts Institute of Technology, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p137-p doi:10.1145/3498685
|
| |
Jacobs, Jules
|
Proc. ACM Program. Lang., vol. 6, issue POPL: "Connectivity Graphs: A Method ..."
Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation Logic
Jules Jacobs, Stephanie Balzer, and Robbert Krebbers
(Radboud University Nijmegen, Netherlands; Carnegie Mellon University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p6-p doi:10.1145/3498662
|
| |
Jang, Junyoung |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Mœbius: Metaprogramming using ..."
Mœbius: Metaprogramming using Contextual Types: The Stage Where System F Can Pattern Match on Itself
Junyoung Jang, Samuel Gélineau, Stefan Monnier, and Brigitte Pientka
(McGill University, Canada; SimSpace, Canada; Université de Montréal, Canada)
Publisher's Version
Article: popl22main-p294-p doi:10.1145/3498700
|
| |
Jeffrey, Alan |
Proc. ACM Program. Lang., vol. 6, issue POPL: "The Leaky Semicolon: Compositional ..."
The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Concurrency
Alan Jeffrey, James Riely, Mark Batty, Simon Cooksey, Ilya Kaysin, and Anton Podkopaev
(Roblox, USA; DePaul University, USA; University of Kent, UK; JetBrains Research, Russia; University of Cambridge, UK; HSE University, Russia)
Publisher's Version
Published Artifact
Artifacts Available
Article: popl22main-p459-p doi:10.1145/3498716
|
| |
Jeon, Minseok |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Return of CFA: Call-Site Sensitivity ..."
Return of CFA: Call-Site Sensitivity Can Be Superior to Object Sensitivity Even for Object-Oriented Programs
Minseok Jeon and Hakjoo Oh
(Korea University, South Korea)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p586-p doi:10.1145/3498720
|
| |
Jha, Somesh |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Interval Universal Approximation ..."
Interval Universal Approximation for Neural Networks
Zi Wang, Aws Albarghouthi, Gautam Prakriya, and Somesh Jha
(University of Wisconsin-Madison, USA; Chinese University of Hong Kong, China; University of Wisconsin, USA)
Publisher's Version
Archive submitted (830 kB)
Article: popl22main-p61-p doi:10.1145/3498675
|
| |
Jhala, Ranjit |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Isolation without Taxation: ..."
Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFI
Matthew Kolosick, Shravan Narayan, Evan Johnson, Conrad Watt, Michael LeMay, Deepak Garg, Ranjit Jhala, and Deian Stefan
(University of California at San Diego, USA; University of Cambridge, UK; Intel Labs, USA; MPI-SWS, Germany)
Publisher's Version
Article: popl22main-p151-p doi:10.1145/3498688
|
| |
Jia, Xiaodong |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Semantics for Variational ..."
Semantics for Variational Quantum Programming
Xiaodong Jia, Andre Kornell, Bert Lindenhovius, Michael Mislove, and Vladimir Zamdzhiev
(Hunan University, China; Tulane University, USA; JKU Linz, Austria; Inria, France)
Publisher's Version
Article: popl22main-p149-p doi:10.1145/3498687
|
| |
Johnson, Evan |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Isolation without Taxation: ..."
Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFI
Matthew Kolosick, Shravan Narayan, Evan Johnson, Conrad Watt, Michael LeMay, Deepak Garg, Ranjit Jhala, and Deian Stefan
(University of California at San Diego, USA; University of Cambridge, UK; Intel Labs, USA; MPI-SWS, Germany)
Publisher's Version
Article: popl22main-p151-p doi:10.1145/3498688
|
| |
Jung, Ralf |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Simuliris: A Separation Logic ..."
Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations
Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, and Derek Dreyer
(MPI-SWS, Germany; Radboud University Nijmegen, Netherlands; KAIST, South Korea)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p158-p doi:10.1145/3498689
|
| |
K, Hari Govind V
|
Proc. ACM Program. Lang., vol. 6, issue POPL: "Solving Constrained Horn Clauses ..."
Solving Constrained Horn Clauses Modulo Algebraic Data Types and Recursive Functions
Hari Govind V K, Sharon Shoham, and Arie Gurfinkel
(University of Waterloo, Canada; Tel Aviv University, Israel)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p629-p doi:10.1145/3498722
|
| |
Kaarsgaard, Robin |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Quantum Information Effects ..."
Quantum Information Effects
Chris Heunen and Robin Kaarsgaard
(University of Edinburgh, UK)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p9-p doi:10.1145/3498663
|
| |
Kammar, Ohad |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Fully Abstract Models for ..."
Fully Abstract Models for Effectful λ-Calculi via Category-Theoretic Logical Relations
Ohad Kammar, Shin-ya Katsumata, and Philip Saville
(University of Edinburgh, UK; National Institute of Informatics, Japan; University of Oxford, UK)
Publisher's Version
Article: popl22main-p331-p doi:10.1145/3498705
|
| |
Kan, Shuanglong |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Solving String Constraints ..."
Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables
Taolue Chen, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu
(Birkbeck University of London, UK; Royal Holloway University of London, UK; Tsinghua University, China; Institute of Software at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; TU Kaiserslautern, Germany; MPI-SWS, Germany; Uppsala University, Sweden)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p350-p doi:10.1145/3498707
|
| |
Kang, Jeehoon |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Simuliris: A Separation Logic ..."
Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations
Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, and Derek Dreyer
(MPI-SWS, Germany; Radboud University Nijmegen, Netherlands; KAIST, South Korea)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p158-p doi:10.1145/3498689
|
| |
Karimov, Toghrul |
Proc. ACM Program. Lang., vol. 6, issue POPL: "What’s Decidable about Linear ..."
What’s Decidable about Linear Loops?
Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, David Purser, Anton Varonka, Markus A. Whiteland, and James Worrell
(MPI-SWS, Germany; University of Oxford, UK)
Publisher's Version
Article: popl22main-p767-p doi:10.1145/3498727
|
| |
Karwowski, Jacek |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Symmetries in Reversible Programming: ..."
Symmetries in Reversible Programming: From Symmetric Rig Groupoids to Reversible Programming Languages
Vikraman Choudhury, Jacek Karwowski, and Amr Sabry
(Indiana University, USA; University of Cambridge, UK; University of Warsaw, Poland)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p31-p doi:10.1145/3498667
|
| |
Katsumata, Shin-ya |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Fully Abstract Models for ..."
Fully Abstract Models for Effectful λ-Calculi via Category-Theoretic Logical Relations
Ohad Kammar, Shin-ya Katsumata, and Philip Saville
(University of Edinburgh, UK; National Institute of Informatics, Japan; University of Oxford, UK)
Publisher's Version
Article: popl22main-p331-p doi:10.1145/3498705
|
| |
Kaysin, Ilya |
Proc. ACM Program. Lang., vol. 6, issue POPL: "The Leaky Semicolon: Compositional ..."
The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Concurrency
Alan Jeffrey, James Riely, Mark Batty, Simon Cooksey, Ilya Kaysin, and Anton Podkopaev
(Roblox, USA; DePaul University, USA; University of Kent, UK; JetBrains Research, Russia; University of Cambridge, UK; HSE University, Russia)
Publisher's Version
Published Artifact
Artifacts Available
Article: popl22main-p459-p doi:10.1145/3498716
|
| |
Kesner, Delia |
Proc. ACM Program. Lang., vol. 6, issue POPL: "A Fine-Grained Computational ..."
A Fine-Grained Computational Interpretation of Girard’s Intuitionistic Proof-Nets
Delia Kesner
(Université de Paris, France; CNRS, France; IRIF, France; Institut Universitaire de France, France)
Publisher's Version
Article: popl22main-p42-p doi:10.1145/3498669
|
| |
Kjaer, Maxime |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Type-Level Programming with ..."
Type-Level Programming with Match Types
Olivier Blanvillain, Jonathan Immanuel Brachthäuser, Maxime Kjaer, and Martin Odersky
(EPFL, Switzerland; University of Tübingen, Germany)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p258-p doi:10.1145/3498698
|
| |
Kjelstrøm, Adam Husted |
Proc. ACM Program. Lang., vol. 6, issue POPL: "The Decidability and Complexity ..."
The Decidability and Complexity of Interleaved Bidirected Dyck Reachability
Adam Husted Kjelstrøm and Andreas Pavlogiannis
(Aarhus University, Denmark)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p55-p doi:10.1145/3498673
|
| |
Koenig, Jason R. |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Induction Duality: Primal-Dual ..."
Induction Duality: Primal-Dual Search for Invariants
Oded Padon, James R. Wilcox, Jason R. Koenig, Kenneth L. McMillan, and Alex Aiken
(VMware Research, USA; Stanford University, USA; Certora, USA; University of Texas at Austin, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Article: popl22main-p428-p doi:10.1145/3498712
|
| |
Koenig, Jérémie |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Verified Compilation of C ..."
Verified Compilation of C Programs with a Nominal Memory Model
Yuting Wang, Ling Zhang, Zhong Shao, and Jérémie Koenig
(Shanghai Jiao Tong University, China; Yale University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p143-p doi:10.1145/3498686
Proc. ACM Program. Lang., vol. 6, issue POPL: "Layered and Object-Based Game ..."
Layered and Object-Based Game Semantics
Arthur Oliveira Vale, Paul-André Melliès, Zhong Shao, Jérémie Koenig, and Léo Stefanesco
(Yale University, USA; CNRS, France; Université de Paris, France; MPI-SWS, Germany)
Publisher's Version
Article: popl22main-p327-p doi:10.1145/3498703
|
| |
Kokologiannakis, Michalis |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Truly Stateless, Optimal Dynamic ..."
Truly Stateless, Optimal Dynamic Partial Order Reduction
Michalis Kokologiannakis, Iason Marmanis, Vladimir Gladstein, and Viktor Vafeiadis
(MPI-SWS, Germany; St. Petersburg University, Russia; JetBrains Research, Russia)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p424-p doi:10.1145/3498711
|
| |
Kolosick, Matthew |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Isolation without Taxation: ..."
Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFI
Matthew Kolosick, Shravan Narayan, Evan Johnson, Conrad Watt, Michael LeMay, Deepak Garg, Ranjit Jhala, and Deian Stefan
(University of California at San Diego, USA; University of Cambridge, UK; Intel Labs, USA; MPI-SWS, Germany)
Publisher's Version
Article: popl22main-p151-p doi:10.1145/3498688
|
| |
Kornell, Andre |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Semantics for Variational ..."
Semantics for Variational Quantum Programming
Xiaodong Jia, Andre Kornell, Bert Lindenhovius, Michael Mislove, and Vladimir Zamdzhiev
(Hunan University, China; Tulane University, USA; JKU Linz, Austria; Inria, France)
Publisher's Version
Article: popl22main-p149-p doi:10.1145/3498687
|
| |
Krawiec, Faustyna |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Provably Correct, Asymptotically ..."
Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic Differentiation
Faustyna Krawiec, Simon Peyton Jones, Neel Krishnaswami, Tom Ellis, Richard A. Eisenberg, and Andrew Fitzgibbon
(University of Cambridge, UK; Microsoft Research, UK; Tweag, France)
Publisher's Version
Article: popl22main-p397-p doi:10.1145/3498710
|
| |
Krebbers, Robbert |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Connectivity Graphs: A Method ..."
Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation Logic
Jules Jacobs, Stephanie Balzer, and Robbert Krebbers
(Radboud University Nijmegen, Netherlands; Carnegie Mellon University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p6-p doi:10.1145/3498662
Proc. ACM Program. Lang., vol. 6, issue POPL: "VIP: Verifying Real-World ..."
VIP: Verifying Real-World C Idioms with Integer-Pointer Casts
Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, and Peter Sewell
(MPI-SWS, Germany; University of Cambridge, UK; Radboud University Nijmegen, Netherlands)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p95-p doi:10.1145/3498681
Proc. ACM Program. Lang., vol. 6, issue POPL: "Simuliris: A Separation Logic ..."
Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations
Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, and Derek Dreyer
(MPI-SWS, Germany; Radboud University Nijmegen, Netherlands; KAIST, South Korea)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p158-p doi:10.1145/3498689
|
| |
Krebs, Matthias |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Dependently-Typed Data Plane ..."
Dependently-Typed Data Plane Programming
Matthias Eichholz, Eric Hayden Campbell, Matthias Krebs, Nate Foster, and Mira Mezini
(TU Darmstadt, Germany; Cornell University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Article: popl22main-p311-p doi:10.1145/3498701
|
| |
Krishnaswami, Neel |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Provably Correct, Asymptotically ..."
Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic Differentiation
Faustyna Krawiec, Simon Peyton Jones, Neel Krishnaswami, Tom Ellis, Richard A. Eisenberg, and Andrew Fitzgibbon
(University of Cambridge, UK; Microsoft Research, UK; Tweag, France)
Publisher's Version
Article: popl22main-p397-p doi:10.1145/3498710
|
| |
Krogmeier, Paul |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Learning Formulas in Finite ..."
Learning Formulas in Finite Variable Logics
Paul Krogmeier and P. Madhusudan
(University of Illinois at Urbana-Champaign, USA)
Publisher's Version
Article: popl22main-p48-p doi:10.1145/3498671
|
| |
Lahiri, Shuvendu K.
|
Proc. ACM Program. Lang., vol. 6, issue POPL: "SolType: Refinement Types ..."
SolType: Refinement Types for Arithmetic Overflow in Solidity
Bryan Tan, Benjamin Mariano, Shuvendu K. Lahiri, Isil Dillig, and Yu Feng
(University of California at Santa Barbara, USA; University of Texas at Austin, USA; Microsoft Research, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p27-p doi:10.1145/3498665
|
| |
Laurel, Jacob |
Proc. ACM Program. Lang., vol. 6, issue POPL: "A Dual Number Abstraction ..."
A Dual Number Abstraction for Static Analysis of Clarke Jacobians
Jacob Laurel, Rem Yang, Gagandeep Singh, and Sasa Misailovic
(University of Illinois at Urbana-Champaign, USA; VMware, USA)
Publisher's Version
Article: popl22main-p542-p doi:10.1145/3498718
|
| |
Laurent, Mickaël |
Proc. ACM Program. Lang., vol. 6, issue POPL: "On Type-Cases, Union Elimination, ..."
On Type-Cases, Union Elimination, and Occurrence Typing
Giuseppe Castagna, Mickaël Laurent, Kim Nguyễn, and Matthew Lutze
(CNRS, France; Université de Paris, France; Université Paris-Saclay, France)
Publisher's Version
Published Artifact
Archive submitted (1.1 MB)
Artifacts Available
Artifacts Reusable
Article: popl22main-p58-p doi:10.1145/3498674
|
| |
Le, Xuan-Bach |
Proc. ACM Program. Lang., vol. 6, issue POPL: "A Quantum Interpretation of ..."
A Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantum Programs Based on Separation Logic
Xuan-Bach Le, Shang-Wei Lin, Jun Sun, and David Sanan
(Nanyang Technological University, Singapore; Singapore Management University, Singapore)
Publisher's Version
Article: popl22main-p247-p doi:10.1145/3498697
|
| |
Lefaucheux, Engel |
Proc. ACM Program. Lang., vol. 6, issue POPL: "What’s Decidable about Linear ..."
What’s Decidable about Linear Loops?
Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, David Purser, Anton Varonka, Markus A. Whiteland, and James Worrell
(MPI-SWS, Germany; University of Oxford, UK)
Publisher's Version
Article: popl22main-p767-p doi:10.1145/3498727
|
| |
LeMay, Michael |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Isolation without Taxation: ..."
Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFI
Matthew Kolosick, Shravan Narayan, Evan Johnson, Conrad Watt, Michael LeMay, Deepak Garg, Ranjit Jhala, and Deian Stefan
(University of California at San Diego, USA; University of Cambridge, UK; Intel Labs, USA; MPI-SWS, Germany)
Publisher's Version
Article: popl22main-p151-p doi:10.1145/3498688
|
| |
Lepigre, Rodolphe |
Proc. ACM Program. Lang., vol. 6, issue POPL: "VIP: Verifying Real-World ..."
VIP: Verifying Real-World C Idioms with Integer-Pointer Casts
Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, and Peter Sewell
(MPI-SWS, Germany; University of Cambridge, UK; Radboud University Nijmegen, Netherlands)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p95-p doi:10.1145/3498681
|
| |
Li, Yuanbo |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Efficient Algorithms for Dynamic ..."
Efficient Algorithms for Dynamic Bidirected Dyck-Reachability
Yuanbo Li, Kris Satya, and Qirun Zhang
(Georgia Institute of Technology, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p725-p doi:10.1145/3498724
|
| |
Lim, Jay P. |
Proc. ACM Program. Lang., vol. 6, issue POPL: "One Polynomial Approximation ..."
One Polynomial Approximation to Produce Correctly Rounded Results of an Elementary Function for Multiple Representations and Rounding Modes
Jay P. Lim and Santosh Nagarakatte
(Rutgers University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p25-p doi:10.1145/3498664
|
| |
Lin, Anthony W. |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Solving String Constraints ..."
Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables
Taolue Chen, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu
(Birkbeck University of London, UK; Royal Holloway University of London, UK; Tsinghua University, China; Institute of Software at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; TU Kaiserslautern, Germany; MPI-SWS, Germany; Uppsala University, Sweden)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p350-p doi:10.1145/3498707
|
| |
Lin, Shang-Wei |
Proc. ACM Program. Lang., vol. 6, issue POPL: "A Quantum Interpretation of ..."
A Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantum Programs Based on Separation Logic
Xuan-Bach Le, Shang-Wei Lin, Jun Sun, and David Sanan
(Nanyang Technological University, Singapore; Singapore Management University, Singapore)
Publisher's Version
Article: popl22main-p247-p doi:10.1145/3498697
|
| |
Lindenhovius, Bert |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Semantics for Variational ..."
Semantics for Variational Quantum Programming
Xiaodong Jia, Andre Kornell, Bert Lindenhovius, Michael Mislove, and Vladimir Zamdzhiev
(Hunan University, China; Tulane University, USA; JKU Linz, Austria; Inria, France)
Publisher's Version
Article: popl22main-p149-p doi:10.1145/3498687
|
| |
Liu, Amanda |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Verified Tensor-Program Optimization ..."
Verified Tensor-Program Optimization Via High-Level Scheduling Rewrites
Amanda Liu, Gilbert Louis Bernstein, Adam Chlipala, and Jonathan Ragan-Kelley
(Massachusetts Institute of Technology, USA; University of California at Berkeley, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p523-p doi:10.1145/3498717
|
| |
Loehr, Devon |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Safe, Modular Packet Pipeline ..."
Safe, Modular Packet Pipeline Programming
Devon Loehr and David Walker
(Princeton University, USA)
Publisher's Version
Published Artifact
Archive submitted (760 kB)
Artifacts Available
Artifacts Reusable
Article: popl22main-p275-p doi:10.1145/3498699
|
| |
Löh, Andres |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Staging with Class: A Specification ..."
Staging with Class: A Specification for Typed Template Haskell
Ningning Xie, Matthew Pickering, Andres Löh, Nicolas Wu, Jeremy Yallop, and Meng Wang
(University of Cambridge, UK; Well-Typed LLP, UK; Imperial College London, UK; University of Bristol, UK)
Publisher's Version
Article: popl22main-p706-p doi:10.1145/3498723
|
| |
Lutze, Matthew |
Proc. ACM Program. Lang., vol. 6, issue POPL: "On Type-Cases, Union Elimination, ..."
On Type-Cases, Union Elimination, and Occurrence Typing
Giuseppe Castagna, Mickaël Laurent, Kim Nguyễn, and Matthew Lutze
(CNRS, France; Université de Paris, France; Université Paris-Saclay, France)
Publisher's Version
Published Artifact
Archive submitted (1.1 MB)
Artifacts Available
Artifacts Reusable
Article: popl22main-p58-p doi:10.1145/3498674
|
| |
Madhusudan, P.
|
Proc. ACM Program. Lang., vol. 6, issue POPL: "Learning Formulas in Finite ..."
Learning Formulas in Finite Variable Logics
Paul Krogmeier and P. Madhusudan
(University of Illinois at Urbana-Champaign, USA)
Publisher's Version
Article: popl22main-p48-p doi:10.1145/3498671
|
| |
Madiot, Jean-Marie |
Proc. ACM Program. Lang., vol. 6, issue POPL: "A Separation Logic for Heap ..."
A Separation Logic for Heap Space under Garbage Collection
Jean-Marie Madiot and François Pottier
(Inria, France)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p49-p doi:10.1145/3498672
|
| |
Majumdar, Rupak |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Context-Bounded Verification ..."
Context-Bounded Verification of Thread Pools
Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche
(MPI-SWS, Germany)
Publisher's Version
Article: popl22main-p90-p doi:10.1145/3498678
Proc. ACM Program. Lang., vol. 6, issue POPL: "Subcubic Certificates for ..."
Subcubic Certificates for CFL Reachability
Dmitry Chistikov, Rupak Majumdar, and Philipp Schepper
(University of Warwick, UK; MPI-SWS, Germany; CISPA, Germany)
Publisher's Version
Article: popl22main-p322-p doi:10.1145/3498702
|
| |
Makarchuk, Gleb |
Proc. ACM Program. Lang., vol. 6, issue POPL: "PRIMA: General and Precise ..."
PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations
Mark Niklas Müller, Gleb Makarchuk, Gagandeep Singh, Markus Püschel, and Martin Vechev
(ETH Zurich, Switzerland; VMware Research, USA; University of Illinois at Urbana-Champaign, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p329-p doi:10.1145/3498704
|
| |
Maranget, Luc |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Extending Intel-x86 Consistency ..."
Extending Intel-x86 Consistency and Persistency: Formalising the Semantics of Intel-x86 Memory Types and Non-temporal Stores
Azalea Raad, Luc Maranget, and Viktor Vafeiadis
(Imperial College London, UK; Inria, France; MPI-SWS, Germany)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p126-p doi:10.1145/3498683
|
| |
Mariano, Benjamin |
Proc. ACM Program. Lang., vol. 6, issue POPL: "SolType: Refinement Types ..."
SolType: Refinement Types for Arithmetic Overflow in Solidity
Bryan Tan, Benjamin Mariano, Shuvendu K. Lahiri, Isil Dillig, and Yu Feng
(University of California at Santa Barbara, USA; University of Texas at Austin, USA; Microsoft Research, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p27-p doi:10.1145/3498665
|
| |
Marmanis, Iason |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Truly Stateless, Optimal Dynamic ..."
Truly Stateless, Optimal Dynamic Partial Order Reduction
Michalis Kokologiannakis, Iason Marmanis, Vladimir Gladstein, and Viktor Vafeiadis
(MPI-SWS, Germany; St. Petersburg University, Russia; JetBrains Research, Russia)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p424-p doi:10.1145/3498711
|
| |
McMillan, Kenneth L. |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Induction Duality: Primal-Dual ..."
Induction Duality: Primal-Dual Search for Invariants
Oded Padon, James R. Wilcox, Jason R. Koenig, Kenneth L. McMillan, and Alex Aiken
(VMware Research, USA; Stanford University, USA; Certora, USA; University of Texas at Austin, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Article: popl22main-p428-p doi:10.1145/3498712
|
| |
McNally, Christopher |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Twist: Sound Reasoning for ..."
Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs
Charles Yuan, Christopher McNally, and Michael Carbin
(Massachusetts Institute of Technology, USA)
Publisher's Version
Published Artifact
Archive submitted (690 kB)
Artifacts Available
Artifacts Reusable
Article: popl22main-p167-p doi:10.1145/3498691
|
| |
Melliès, Paul-André |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Layered and Object-Based Game ..."
Layered and Object-Based Game Semantics
Arthur Oliveira Vale, Paul-André Melliès, Zhong Shao, Jérémie Koenig, and Léo Stefanesco
(Yale University, USA; CNRS, France; Université de Paris, France; MPI-SWS, Germany)
Publisher's Version
Article: popl22main-p327-p doi:10.1145/3498703
|
| |
Memarian, Kayvan |
Proc. ACM Program. Lang., vol. 6, issue POPL: "VIP: Verifying Real-World ..."
VIP: Verifying Real-World C Idioms with Integer-Pointer Casts
Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, and Peter Sewell
(MPI-SWS, Germany; University of Cambridge, UK; Radboud University Nijmegen, Netherlands)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p95-p doi:10.1145/3498681
|
| |
Mestre, Julián |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Profile Inference Revisited ..."
Profile Inference Revisited
Wenlei He, Julián Mestre, Sergey Pupyrev, Lei Wang, and Hongtao Yu
(Facebook, USA; University of Sydney, Australia)
Publisher's Version
Article: popl22main-p431-p doi:10.1145/3498714
|
| |
Mezini, Mira |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Dependently-Typed Data Plane ..."
Dependently-Typed Data Plane Programming
Matthias Eichholz, Eric Hayden Campbell, Matthias Krebs, Nate Foster, and Mira Mezini
(TU Darmstadt, Germany; Cornell University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Article: popl22main-p311-p doi:10.1145/3498701
|
| |
Miltner, Anders |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Bottom-Up Synthesis of Recursive ..."
Bottom-Up Synthesis of Recursive Functional Programs using Angelic Execution
Anders Miltner, Adrian Trejo Nuñez, Ana Brendel, Swarat Chaudhuri, and Isil Dillig
(University of Texas at Austin, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p124-p doi:10.1145/3498682
|
| |
Misailovic, Sasa |
Proc. ACM Program. Lang., vol. 6, issue POPL: "A Dual Number Abstraction ..."
A Dual Number Abstraction for Static Analysis of Clarke Jacobians
Jacob Laurel, Rem Yang, Gagandeep Singh, and Sasa Misailovic
(University of Illinois at Urbana-Champaign, USA; VMware, USA)
Publisher's Version
Article: popl22main-p542-p doi:10.1145/3498718
|
| |
Mislove, Michael |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Semantics for Variational ..."
Semantics for Variational Quantum Programming
Xiaodong Jia, Andre Kornell, Bert Lindenhovius, Michael Mislove, and Vladimir Zamdzhiev
(Hunan University, China; Tulane University, USA; JKU Linz, Austria; Inria, France)
Publisher's Version
Article: popl22main-p149-p doi:10.1145/3498687
|
| |
Monnier, Stefan |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Mœbius: Metaprogramming using ..."
Mœbius: Metaprogramming using Contextual Types: The Stage Where System F Can Pattern Match on Itself
Junyoung Jang, Samuel Gélineau, Stefan Monnier, and Brigitte Pientka
(McGill University, Canada; SimSpace, Canada; Université de Montréal, Canada)
Publisher's Version
Article: popl22main-p294-p doi:10.1145/3498700
|
| |
Müller, Mark Niklas |
Proc. ACM Program. Lang., vol. 6, issue POPL: "PRIMA: General and Precise ..."
PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations
Mark Niklas Müller, Gleb Makarchuk, Gagandeep Singh, Markus Püschel, and Martin Vechev
(ETH Zurich, Switzerland; VMware Research, USA; University of Illinois at Urbana-Champaign, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p329-p doi:10.1145/3498704
|
| |
Muller, Stefan K. |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Static Prediction of Parallel ..."
Static Prediction of Parallel Computation Graphs
Stefan K. Muller
(Illinois Institute of Technology, USA)
Publisher's Version
Archive submitted (900 kB)
Article: popl22main-p383-p doi:10.1145/3498708
|
| |
Nagarakatte, Santosh
|
Proc. ACM Program. Lang., vol. 6, issue POPL: "One Polynomial Approximation ..."
One Polynomial Approximation to Produce Correctly Rounded Results of an Elementary Function for Multiple Representations and Rounding Modes
Jay P. Lim and Santosh Nagarakatte
(Rutgers University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p25-p doi:10.1145/3498664
|
| |
Nanevski, Aleksandar |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Visibility Reasoning for Concurrent ..."
Visibility Reasoning for Concurrent Snapshot Algorithms
Joakim Öhman and Aleksandar Nanevski
(IMDEA Software Institute, Spain; Universidad Politécnica de Madrid, Spain)
Publisher's Version
Archive submitted (530 kB)
Article: popl22main-p206-p doi:10.1145/3498694
|
| |
Narayan, Shravan |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Isolation without Taxation: ..."
Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFI
Matthew Kolosick, Shravan Narayan, Evan Johnson, Conrad Watt, Michael LeMay, Deepak Garg, Ranjit Jhala, and Deian Stefan
(University of California at San Diego, USA; University of Cambridge, UK; Intel Labs, USA; MPI-SWS, Germany)
Publisher's Version
Article: popl22main-p151-p doi:10.1145/3498688
|
| |
Nelson, Luke |
Proc. ACM Program. Lang., vol. 6, issue POPL: "A Formal Foundation for Symbolic ..."
A Formal Foundation for Symbolic Evaluation with Merging
Sorawee Porncharoenwase, Luke Nelson, Xi Wang, and Emina Torlak
(University of Washington, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p390-p doi:10.1145/3498709
|
| |
Nguyen, Minh |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Linked Visualisations via ..."
Linked Visualisations via Galois Dependencies
Roly Perera, Minh Nguyen, Tomas Petricek, and Meng Wang
(Alan Turing Institute, UK; University of Bristol, UK; University of Kent, UK)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p34-p doi:10.1145/3498668
|
| |
Nguyễn, Kim |
Proc. ACM Program. Lang., vol. 6, issue POPL: "On Type-Cases, Union Elimination, ..."
On Type-Cases, Union Elimination, and Occurrence Typing
Giuseppe Castagna, Mickaël Laurent, Kim Nguyễn, and Matthew Lutze
(CNRS, France; Université de Paris, France; Université Paris-Saclay, France)
Publisher's Version
Published Artifact
Archive submitted (1.1 MB)
Artifacts Available
Artifacts Reusable
Article: popl22main-p58-p doi:10.1145/3498674
|
| |
Niu, Yue |
Proc. ACM Program. Lang., vol. 6, issue POPL: "A Cost-Aware Logical Framework ..."
A Cost-Aware Logical Framework
Yue Niu, Jonathan Sterling, Harrison Grodin, and Robert Harper
(Carnegie Mellon University, USA; Aarhus University, Denmark)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p47-p doi:10.1145/3498670
|
| |
Nuñez, Adrian Trejo |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Bottom-Up Synthesis of Recursive ..."
Bottom-Up Synthesis of Recursive Functional Programs using Angelic Execution
Anders Miltner, Adrian Trejo Nuñez, Ana Brendel, Swarat Chaudhuri, and Isil Dillig
(University of Texas at Austin, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p124-p doi:10.1145/3498682
|
| |
Odersky, Martin
|
Proc. ACM Program. Lang., vol. 6, issue POPL: "Type-Level Programming with ..."
Type-Level Programming with Match Types
Olivier Blanvillain, Jonathan Immanuel Brachthäuser, Maxime Kjaer, and Martin Odersky
(EPFL, Switzerland; University of Tübingen, Germany)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p258-p doi:10.1145/3498698
|
| |
Oh, Hakjoo |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Return of CFA: Call-Site Sensitivity ..."
Return of CFA: Call-Site Sensitivity Can Be Superior to Object Sensitivity Even for Object-Oriented Programs
Minseok Jeon and Hakjoo Oh
(Korea University, South Korea)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p586-p doi:10.1145/3498720
|
| |
O'Hearn, Peter W. |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Concurrent Incorrectness Separation ..."
Concurrent Incorrectness Separation Logic
Azalea Raad, Josh Berdine, Derek Dreyer, and Peter W. O'Hearn
(Imperial College London, UK; Meta, UK; MPI-SWS, Germany; University College London, UK)
Publisher's Version
Article: popl22main-p233-p doi:10.1145/3498695
|
| |
Öhman, Joakim |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Visibility Reasoning for Concurrent ..."
Visibility Reasoning for Concurrent Snapshot Algorithms
Joakim Öhman and Aleksandar Nanevski
(IMDEA Software Institute, Spain; Universidad Politécnica de Madrid, Spain)
Publisher's Version
Archive submitted (530 kB)
Article: popl22main-p206-p doi:10.1145/3498694
|
| |
Oliveira Vale, Arthur |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Layered and Object-Based Game ..."
Layered and Object-Based Game Semantics
Arthur Oliveira Vale, Paul-André Melliès, Zhong Shao, Jérémie Koenig, and Léo Stefanesco
(Yale University, USA; CNRS, France; Université de Paris, France; MPI-SWS, Germany)
Publisher's Version
Article: popl22main-p327-p doi:10.1145/3498703
|
| |
Ouaknine, Joël |
Proc. ACM Program. Lang., vol. 6, issue POPL: "What’s Decidable about Linear ..."
What’s Decidable about Linear Loops?
Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, David Purser, Anton Varonka, Markus A. Whiteland, and James Worrell
(MPI-SWS, Germany; University of Oxford, UK)
Publisher's Version
Article: popl22main-p767-p doi:10.1145/3498727
|
| |
Padon, Oded
|
Proc. ACM Program. Lang., vol. 6, issue POPL: "Induction Duality: Primal-Dual ..."
Induction Duality: Primal-Dual Search for Invariants
Oded Padon, James R. Wilcox, Jason R. Koenig, Kenneth L. McMillan, and Alex Aiken
(VMware Research, USA; Stanford University, USA; Certora, USA; University of Texas at Austin, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Article: popl22main-p428-p doi:10.1145/3498712
|
| |
Padovani, Luca |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Fair Termination of Binary ..."
Fair Termination of Binary Sessions
Luca Ciccone and Luca Padovani
(University of Turin, Italy)
Publisher's Version
Published Artifact
Archive submitted (600 kB)
Artifacts Available
Artifacts Reusable
Article: popl22main-p30-p doi:10.1145/3498666
|
| |
Pavlogiannis, Andreas |
Proc. ACM Program. Lang., vol. 6, issue POPL: "The Decidability and Complexity ..."
The Decidability and Complexity of Interleaved Bidirected Dyck Reachability
Adam Husted Kjelstrøm and Andreas Pavlogiannis
(Aarhus University, Denmark)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p55-p doi:10.1145/3498673
|
| |
Perera, Roly |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Linked Visualisations via ..."
Linked Visualisations via Galois Dependencies
Roly Perera, Minh Nguyen, Tomas Petricek, and Meng Wang
(Alan Turing Institute, UK; University of Bristol, UK; University of Kent, UK)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p34-p doi:10.1145/3498668
|
| |
Petricek, Tomas |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Linked Visualisations via ..."
Linked Visualisations via Galois Dependencies
Roly Perera, Minh Nguyen, Tomas Petricek, and Meng Wang
(Alan Turing Institute, UK; University of Bristol, UK; University of Kent, UK)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p34-p doi:10.1145/3498668
|
| |
Peyton Jones, Simon |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Provably Correct, Asymptotically ..."
Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic Differentiation
Faustyna Krawiec, Simon Peyton Jones, Neel Krishnaswami, Tom Ellis, Richard A. Eisenberg, and Andrew Fitzgibbon
(University of Cambridge, UK; Microsoft Research, UK; Tweag, France)
Publisher's Version
Article: popl22main-p397-p doi:10.1145/3498710
|
| |
Pickering, Matthew |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Staging with Class: A Specification ..."
Staging with Class: A Specification for Typed Template Haskell
Ningning Xie, Matthew Pickering, Andres Löh, Nicolas Wu, Jeremy Yallop, and Meng Wang
(University of Cambridge, UK; Well-Typed LLP, UK; Imperial College London, UK; University of Bristol, UK)
Publisher's Version
Article: popl22main-p706-p doi:10.1145/3498723
|
| |
Pientka, Brigitte |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Mœbius: Metaprogramming using ..."
Mœbius: Metaprogramming using Contextual Types: The Stage Where System F Can Pattern Match on Itself
Junyoung Jang, Samuel Gélineau, Stefan Monnier, and Brigitte Pientka
(McGill University, Canada; SimSpace, Canada; Université de Montréal, Canada)
Publisher's Version
Article: popl22main-p294-p doi:10.1145/3498700
|
| |
Podkopaev, Anton |
Proc. ACM Program. Lang., vol. 6, issue POPL: "The Leaky Semicolon: Compositional ..."
The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Concurrency
Alan Jeffrey, James Riely, Mark Batty, Simon Cooksey, Ilya Kaysin, and Anton Podkopaev
(Roblox, USA; DePaul University, USA; University of Kent, UK; JetBrains Research, Russia; University of Cambridge, UK; HSE University, Russia)
Publisher's Version
Published Artifact
Artifacts Available
Article: popl22main-p459-p doi:10.1145/3498716
|
| |
Porncharoenwase, Sorawee |
Proc. ACM Program. Lang., vol. 6, issue POPL: "A Formal Foundation for Symbolic ..."
A Formal Foundation for Symbolic Evaluation with Merging
Sorawee Porncharoenwase, Luke Nelson, Xi Wang, and Emina Torlak
(University of Washington, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p390-p doi:10.1145/3498709
|
| |
Pottier, François |
Proc. ACM Program. Lang., vol. 6, issue POPL: "A Separation Logic for Heap ..."
A Separation Logic for Heap Space under Garbage Collection
Jean-Marie Madiot and François Pottier
(Inria, France)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p49-p doi:10.1145/3498672
|
| |
Prakriya, Gautam |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Interval Universal Approximation ..."
Interval Universal Approximation for Neural Networks
Zi Wang, Aws Albarghouthi, Gautam Prakriya, and Somesh Jha
(University of Wisconsin-Madison, USA; Chinese University of Hong Kong, China; University of Wisconsin, USA)
Publisher's Version
Archive submitted (830 kB)
Article: popl22main-p61-p doi:10.1145/3498675
|
| |
Pujet, Loïc |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Observational Equality: Now ..."
Observational Equality: Now for Good
Loïc Pujet and Nicolas Tabareau
(Inria, France)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p191-p doi:10.1145/3498693
|
| |
Pupyrev, Sergey |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Profile Inference Revisited ..."
Profile Inference Revisited
Wenlei He, Julián Mestre, Sergey Pupyrev, Lei Wang, and Hongtao Yu
(Facebook, USA; University of Sydney, Australia)
Publisher's Version
Article: popl22main-p431-p doi:10.1145/3498714
|
| |
Purser, David |
Proc. ACM Program. Lang., vol. 6, issue POPL: "What’s Decidable about Linear ..."
What’s Decidable about Linear Loops?
Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, David Purser, Anton Varonka, Markus A. Whiteland, and James Worrell
(MPI-SWS, Germany; University of Oxford, UK)
Publisher's Version
Article: popl22main-p767-p doi:10.1145/3498727
|
| |
Püschel, Markus |
Proc. ACM Program. Lang., vol. 6, issue POPL: "PRIMA: General and Precise ..."
PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations
Mark Niklas Müller, Gleb Makarchuk, Gagandeep Singh, Markus Püschel, and Martin Vechev
(ETH Zurich, Switzerland; VMware Research, USA; University of Illinois at Urbana-Champaign, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p329-p doi:10.1145/3498704
|
| |
Raad, Azalea
|
Proc. ACM Program. Lang., vol. 6, issue POPL: "Extending Intel-x86 Consistency ..."
Extending Intel-x86 Consistency and Persistency: Formalising the Semantics of Intel-x86 Memory Types and Non-temporal Stores
Azalea Raad, Luc Maranget, and Viktor Vafeiadis
(Imperial College London, UK; Inria, France; MPI-SWS, Germany)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p126-p doi:10.1145/3498683
Proc. ACM Program. Lang., vol. 6, issue POPL: "Concurrent Incorrectness Separation ..."
Concurrent Incorrectness Separation Logic
Azalea Raad, Josh Berdine, Derek Dreyer, and Peter W. O'Hearn
(Imperial College London, UK; Meta, UK; MPI-SWS, Germany; University College London, UK)
Publisher's Version
Article: popl22main-p233-p doi:10.1145/3498695
|
| |
Ragan-Kelley, Jonathan |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Verified Tensor-Program Optimization ..."
Verified Tensor-Program Optimization Via High-Level Scheduling Rewrites
Amanda Liu, Gilbert Louis Bernstein, Adam Chlipala, and Jonathan Ragan-Kelley
(Massachusetts Institute of Technology, USA; University of California at Berkeley, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p523-p doi:10.1145/3498717
|
| |
Riely, James |
Proc. ACM Program. Lang., vol. 6, issue POPL: "The Leaky Semicolon: Compositional ..."
The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Concurrency
Alan Jeffrey, James Riely, Mark Batty, Simon Cooksey, Ilya Kaysin, and Anton Podkopaev
(Roblox, USA; DePaul University, USA; University of Kent, UK; JetBrains Research, Russia; University of Cambridge, UK; HSE University, Russia)
Publisher's Version
Published Artifact
Artifacts Available
Article: popl22main-p459-p doi:10.1145/3498716
|
| |
Rümmer, Philipp |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Solving String Constraints ..."
Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables
Taolue Chen, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu
(Birkbeck University of London, UK; Royal Holloway University of London, UK; Tsinghua University, China; Institute of Software at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; TU Kaiserslautern, Germany; MPI-SWS, Germany; Uppsala University, Sweden)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p350-p doi:10.1145/3498707
|
| |
Sabry, Amr
|
Proc. ACM Program. Lang., vol. 6, issue POPL: "Symmetries in Reversible Programming: ..."
Symmetries in Reversible Programming: From Symmetric Rig Groupoids to Reversible Programming Languages
Vikraman Choudhury, Jacek Karwowski, and Amr Sabry
(Indiana University, USA; University of Cambridge, UK; University of Warsaw, Poland)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p31-p doi:10.1145/3498667
|
| |
Sagiv, Mooly |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Property-Directed Reachability ..."
Property-Directed Reachability as Abstract Interpretation in the Monotone Theory
Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, and James R. Wilcox
(Tel Aviv University, Israel; Certora, USA)
Publisher's Version
Article: popl22main-p65-p doi:10.1145/3498676
|
| |
Sammler, Michael |
Proc. ACM Program. Lang., vol. 6, issue POPL: "VIP: Verifying Real-World ..."
VIP: Verifying Real-World C Idioms with Integer-Pointer Casts
Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, and Peter Sewell
(MPI-SWS, Germany; University of Cambridge, UK; Radboud University Nijmegen, Netherlands)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p95-p doi:10.1145/3498681
Proc. ACM Program. Lang., vol. 6, issue POPL: "Simuliris: A Separation Logic ..."
Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations
Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, and Derek Dreyer
(MPI-SWS, Germany; Radboud University Nijmegen, Netherlands; KAIST, South Korea)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p158-p doi:10.1145/3498689
|
| |
Sanan, David |
Proc. ACM Program. Lang., vol. 6, issue POPL: "A Quantum Interpretation of ..."
A Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantum Programs Based on Separation Logic
Xuan-Bach Le, Shang-Wei Lin, Jun Sun, and David Sanan
(Nanyang Technological University, Singapore; Singapore Management University, Singapore)
Publisher's Version
Article: popl22main-p247-p doi:10.1145/3498697
|
| |
Sangiorgi, Davide |
Proc. ACM Program. Lang., vol. 6, issue POPL: "From Enhanced Coinduction ..."
From Enhanced Coinduction towards Enhanced Induction
Davide Sangiorgi
(University of Bologna, Italy; Inria, France)
Publisher's Version
Archive submitted (300 kB)
Article: popl22main-p93-p doi:10.1145/3498679
|
| |
Satya, Kris |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Efficient Algorithms for Dynamic ..."
Efficient Algorithms for Dynamic Bidirected Dyck-Reachability
Yuanbo Li, Kris Satya, and Qirun Zhang
(Georgia Institute of Technology, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p725-p doi:10.1145/3498724
|
| |
Saville, Philip |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Fully Abstract Models for ..."
Fully Abstract Models for Effectful λ-Calculi via Category-Theoretic Logical Relations
Ohad Kammar, Shin-ya Katsumata, and Philip Saville
(University of Edinburgh, UK; National Institute of Informatics, Japan; University of Oxford, UK)
Publisher's Version
Article: popl22main-p331-p doi:10.1145/3498705
|
| |
Schepper, Philipp |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Subcubic Certificates for ..."
Subcubic Certificates for CFL Reachability
Dmitry Chistikov, Rupak Majumdar, and Philipp Schepper
(University of Warwick, UK; MPI-SWS, Germany; CISPA, Germany)
Publisher's Version
Article: popl22main-p322-p doi:10.1145/3498702
|
| |
Sewell, Peter |
Proc. ACM Program. Lang., vol. 6, issue POPL: "VIP: Verifying Real-World ..."
VIP: Verifying Real-World C Idioms with Integer-Pointer Casts
Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, and Peter Sewell
(MPI-SWS, Germany; University of Cambridge, UK; Radboud University Nijmegen, Netherlands)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p95-p doi:10.1145/3498681
|
| |
Shao, Zhong |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Verified Compilation of C ..."
Verified Compilation of C Programs with a Nominal Memory Model
Yuting Wang, Ling Zhang, Zhong Shao, and Jérémie Koenig
(Shanghai Jiao Tong University, China; Yale University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p143-p doi:10.1145/3498686
Proc. ACM Program. Lang., vol. 6, issue POPL: "Layered and Object-Based Game ..."
Layered and Object-Based Game Semantics
Arthur Oliveira Vale, Paul-André Melliès, Zhong Shao, Jérémie Koenig, and Léo Stefanesco
(Yale University, USA; CNRS, France; Université de Paris, France; MPI-SWS, Germany)
Publisher's Version
Article: popl22main-p327-p doi:10.1145/3498703
|
| |
Shoham, Sharon |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Property-Directed Reachability ..."
Property-Directed Reachability as Abstract Interpretation in the Monotone Theory
Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, and James R. Wilcox
(Tel Aviv University, Israel; Certora, USA)
Publisher's Version
Article: popl22main-p65-p doi:10.1145/3498676
Proc. ACM Program. Lang., vol. 6, issue POPL: "Solving Constrained Horn Clauses ..."
Solving Constrained Horn Clauses Modulo Algebraic Data Types and Recursive Functions
Hari Govind V K, Sharon Shoham, and Arie Gurfinkel
(University of Waterloo, Canada; Tel Aviv University, Israel)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p629-p doi:10.1145/3498722
|
| |
Singh, Gagandeep |
Proc. ACM Program. Lang., vol. 6, issue POPL: "PRIMA: General and Precise ..."
PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations
Mark Niklas Müller, Gleb Makarchuk, Gagandeep Singh, Markus Püschel, and Martin Vechev
(ETH Zurich, Switzerland; VMware Research, USA; University of Illinois at Urbana-Champaign, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p329-p doi:10.1145/3498704
Proc. ACM Program. Lang., vol. 6, issue POPL: "A Dual Number Abstraction ..."
A Dual Number Abstraction for Static Analysis of Clarke Jacobians
Jacob Laurel, Rem Yang, Gagandeep Singh, and Sasa Misailovic
(University of Illinois at Urbana-Champaign, USA; VMware, USA)
Publisher's Version
Article: popl22main-p542-p doi:10.1145/3498718
|
| |
Spies, Simon |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Simuliris: A Separation Logic ..."
Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations
Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, and Derek Dreyer
(MPI-SWS, Germany; Radboud University Nijmegen, Netherlands; KAIST, South Korea)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p158-p doi:10.1145/3498689
|
| |
Stefan, Deian |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Isolation without Taxation: ..."
Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFI
Matthew Kolosick, Shravan Narayan, Evan Johnson, Conrad Watt, Michael LeMay, Deepak Garg, Ranjit Jhala, and Deian Stefan
(University of California at San Diego, USA; University of Cambridge, UK; Intel Labs, USA; MPI-SWS, Germany)
Publisher's Version
Article: popl22main-p151-p doi:10.1145/3498688
|
| |
Stefanesco, Léo |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Layered and Object-Based Game ..."
Layered and Object-Based Game Semantics
Arthur Oliveira Vale, Paul-André Melliès, Zhong Shao, Jérémie Koenig, and Léo Stefanesco
(Yale University, USA; CNRS, France; Université de Paris, France; MPI-SWS, Germany)
Publisher's Version
Article: popl22main-p327-p doi:10.1145/3498703
|
| |
Sterling, Jonathan |
Proc. ACM Program. Lang., vol. 6, issue POPL: "A Cost-Aware Logical Framework ..."
A Cost-Aware Logical Framework
Yue Niu, Jonathan Sterling, Harrison Grodin, and Robert Harper
(Carnegie Mellon University, USA; Aarhus University, Denmark)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p47-p doi:10.1145/3498670
|
| |
Sun, Jun |
Proc. ACM Program. Lang., vol. 6, issue POPL: "A Quantum Interpretation of ..."
A Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantum Programs Based on Separation Logic
Xuan-Bach Le, Shang-Wei Lin, Jun Sun, and David Sanan
(Nanyang Technological University, Singapore; Singapore Management University, Singapore)
Publisher's Version
Article: popl22main-p247-p doi:10.1145/3498697
|
| |
Szamozvancev, Dmitrij |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Formal Metatheory of Second-Order ..."
Formal Metatheory of Second-Order Abstract Syntax
Marcelo Fiore and Dmitrij Szamozvancev
(University of Cambridge, UK)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p437-p doi:10.1145/3498715
|
| |
Tabareau, Nicolas
|
Proc. ACM Program. Lang., vol. 6, issue POPL: "Observational Equality: Now ..."
Observational Equality: Now for Good
Loïc Pujet and Nicolas Tabareau
(Inria, France)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p191-p doi:10.1145/3498693
|
| |
Tan, Bryan |
Proc. ACM Program. Lang., vol. 6, issue POPL: "SolType: Refinement Types ..."
SolType: Refinement Types for Arithmetic Overflow in Solidity
Bryan Tan, Benjamin Mariano, Shuvendu K. Lahiri, Isil Dillig, and Yu Feng
(University of California at Santa Barbara, USA; University of Texas at Austin, USA; Microsoft Research, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p27-p doi:10.1145/3498665
|
| |
Tassarotti, Joseph |
Proc. ACM Program. Lang., vol. 6, issue POPL: "A Separation Logic for Negative ..."
A Separation Logic for Negative Dependence
Jialu Bao, Marco Gaboardi, Justin Hsu, and Joseph Tassarotti
(Cornell University, USA; Boston University, USA; Boston College, USA)
Publisher's Version
Article: popl22main-p550-p doi:10.1145/3498719
|
| |
Tatlock, Zachary |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Relational E-matching ..."
Relational E-matching
Yihong Zhang, Yisu Remy Wang, Max Willsey, and Zachary Tatlock
(University of Washington, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p244-p doi:10.1145/3498696
|
| |
Thinniyam, Ramanathan S. |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Context-Bounded Verification ..."
Context-Bounded Verification of Thread Pools
Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche
(MPI-SWS, Germany)
Publisher's Version
Article: popl22main-p90-p doi:10.1145/3498678
|
| |
Torlak, Emina |
Proc. ACM Program. Lang., vol. 6, issue POPL: "A Formal Foundation for Symbolic ..."
A Formal Foundation for Symbolic Evaluation with Merging
Sorawee Porncharoenwase, Luke Nelson, Xi Wang, and Emina Torlak
(University of Washington, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p390-p doi:10.1145/3498709
|
| |
Tsukada, Takeshi |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Software Model-Checking as ..."
Software Model-Checking as Cyclic-Proof Search
Takeshi Tsukada and Hiroshi Unno
(Chiba University, Japan; University of Tsukuba, Japan; RIKEN AIP, Japan)
Publisher's Version
Article: popl22main-p736-p doi:10.1145/3498725
|
| |
Unno, Hiroshi
|
Proc. ACM Program. Lang., vol. 6, issue POPL: "Software Model-Checking as ..."
Software Model-Checking as Cyclic-Proof Search
Takeshi Tsukada and Hiroshi Unno
(Chiba University, Japan; University of Tsukuba, Japan; RIKEN AIP, Japan)
Publisher's Version
Article: popl22main-p736-p doi:10.1145/3498725
|
| |
Vafeiadis, Viktor
|
Proc. ACM Program. Lang., vol. 6, issue POPL: "Extending Intel-x86 Consistency ..."
Extending Intel-x86 Consistency and Persistency: Formalising the Semantics of Intel-x86 Memory Types and Non-temporal Stores
Azalea Raad, Luc Maranget, and Viktor Vafeiadis
(Imperial College London, UK; Inria, France; MPI-SWS, Germany)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p126-p doi:10.1145/3498683
Proc. ACM Program. Lang., vol. 6, issue POPL: "Truly Stateless, Optimal Dynamic ..."
Truly Stateless, Optimal Dynamic Partial Order Reduction
Michalis Kokologiannakis, Iason Marmanis, Vladimir Gladstein, and Viktor Vafeiadis
(MPI-SWS, Germany; St. Petersburg University, Russia; JetBrains Research, Russia)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p424-p doi:10.1145/3498711
|
| |
Varonka, Anton |
Proc. ACM Program. Lang., vol. 6, issue POPL: "What’s Decidable about Linear ..."
What’s Decidable about Linear Loops?
Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, David Purser, Anton Varonka, Markus A. Whiteland, and James Worrell
(MPI-SWS, Germany; University of Oxford, UK)
Publisher's Version
Article: popl22main-p767-p doi:10.1145/3498727
|
| |
Vechev, Martin |
Proc. ACM Program. Lang., vol. 6, issue POPL: "PRIMA: General and Precise ..."
PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations
Mark Niklas Müller, Gleb Makarchuk, Gagandeep Singh, Markus Püschel, and Martin Vechev
(ETH Zurich, Switzerland; VMware Research, USA; University of Illinois at Urbana-Champaign, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p329-p doi:10.1145/3498704
|
| |
Walker, David
|
Proc. ACM Program. Lang., vol. 6, issue POPL: "Safe, Modular Packet Pipeline ..."
Safe, Modular Packet Pipeline Programming
Devon Loehr and David Walker
(Princeton University, USA)
Publisher's Version
Published Artifact
Archive submitted (760 kB)
Artifacts Available
Artifacts Reusable
Article: popl22main-p275-p doi:10.1145/3498699
|
| |
Wang, Lei |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Profile Inference Revisited ..."
Profile Inference Revisited
Wenlei He, Julián Mestre, Sergey Pupyrev, Lei Wang, and Hongtao Yu
(Facebook, USA; University of Sydney, Australia)
Publisher's Version
Article: popl22main-p431-p doi:10.1145/3498714
|
| |
Wang, Meng |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Staging with Class: A Specification ..."
Staging with Class: A Specification for Typed Template Haskell
Ningning Xie, Matthew Pickering, Andres Löh, Nicolas Wu, Jeremy Yallop, and Meng Wang
(University of Cambridge, UK; Well-Typed LLP, UK; Imperial College London, UK; University of Bristol, UK)
Publisher's Version
Article: popl22main-p706-p doi:10.1145/3498723
Proc. ACM Program. Lang., vol. 6, issue POPL: "Linked Visualisations via ..."
Linked Visualisations via Galois Dependencies
Roly Perera, Minh Nguyen, Tomas Petricek, and Meng Wang
(Alan Turing Institute, UK; University of Bristol, UK; University of Kent, UK)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p34-p doi:10.1145/3498668
|
| |
Wang, Xi |
Proc. ACM Program. Lang., vol. 6, issue POPL: "A Formal Foundation for Symbolic ..."
A Formal Foundation for Symbolic Evaluation with Merging
Sorawee Porncharoenwase, Luke Nelson, Xi Wang, and Emina Torlak
(University of Washington, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p390-p doi:10.1145/3498709
|
| |
Wang, Yisu Remy |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Relational E-matching ..."
Relational E-matching
Yihong Zhang, Yisu Remy Wang, Max Willsey, and Zachary Tatlock
(University of Washington, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p244-p doi:10.1145/3498696
|
| |
Wang, Yuting |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Verified Compilation of C ..."
Verified Compilation of C Programs with a Nominal Memory Model
Yuting Wang, Ling Zhang, Zhong Shao, and Jérémie Koenig
(Shanghai Jiao Tong University, China; Yale University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p143-p doi:10.1145/3498686
|
| |
Wang, Zhuyang |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Logarithm and Program Testing ..."
Logarithm and Program Testing
Kuen-Bang Hou (Favonia) and Zhuyang Wang
(University of Minnesota, USA)
Publisher's Version
Published Artifact
Archive submitted (540 kB)
Artifacts Available
Artifacts Reusable
Article: popl22main-p764-p doi:10.1145/3498726
|
| |
Wang, Zi |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Interval Universal Approximation ..."
Interval Universal Approximation for Neural Networks
Zi Wang, Aws Albarghouthi, Gautam Prakriya, and Somesh Jha
(University of Wisconsin-Madison, USA; Chinese University of Hong Kong, China; University of Wisconsin, USA)
Publisher's Version
Archive submitted (830 kB)
Article: popl22main-p61-p doi:10.1145/3498675
|
| |
Watt, Conrad |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Isolation without Taxation: ..."
Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFI
Matthew Kolosick, Shravan Narayan, Evan Johnson, Conrad Watt, Michael LeMay, Deepak Garg, Ranjit Jhala, and Deian Stefan
(University of California at San Diego, USA; University of Cambridge, UK; Intel Labs, USA; MPI-SWS, Germany)
Publisher's Version
Article: popl22main-p151-p doi:10.1145/3498688
|
| |
Whiteland, Markus A. |
Proc. ACM Program. Lang., vol. 6, issue POPL: "What’s Decidable about Linear ..."
What’s Decidable about Linear Loops?
Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, David Purser, Anton Varonka, Markus A. Whiteland, and James Worrell
(MPI-SWS, Germany; University of Oxford, UK)
Publisher's Version
Article: popl22main-p767-p doi:10.1145/3498727
|
| |
Wilcox, James R. |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Property-Directed Reachability ..."
Property-Directed Reachability as Abstract Interpretation in the Monotone Theory
Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, and James R. Wilcox
(Tel Aviv University, Israel; Certora, USA)
Publisher's Version
Article: popl22main-p65-p doi:10.1145/3498676
Proc. ACM Program. Lang., vol. 6, issue POPL: "Induction Duality: Primal-Dual ..."
Induction Duality: Primal-Dual Search for Invariants
Oded Padon, James R. Wilcox, Jason R. Koenig, Kenneth L. McMillan, and Alex Aiken
(VMware Research, USA; Stanford University, USA; Certora, USA; University of Texas at Austin, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Article: popl22main-p428-p doi:10.1145/3498712
|
| |
Willsey, Max |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Relational E-matching ..."
Relational E-matching
Yihong Zhang, Yisu Remy Wang, Max Willsey, and Zachary Tatlock
(University of Washington, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p244-p doi:10.1145/3498696
|
| |
Worrell, James |
Proc. ACM Program. Lang., vol. 6, issue POPL: "What’s Decidable about Linear ..."
What’s Decidable about Linear Loops?
Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, David Purser, Anton Varonka, Markus A. Whiteland, and James Worrell
(MPI-SWS, Germany; University of Oxford, UK)
Publisher's Version
Article: popl22main-p767-p doi:10.1145/3498727
|
| |
Wu, Nicolas |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Staging with Class: A Specification ..."
Staging with Class: A Specification for Typed Template Haskell
Ningning Xie, Matthew Pickering, Andres Löh, Nicolas Wu, Jeremy Yallop, and Meng Wang
(University of Cambridge, UK; Well-Typed LLP, UK; Imperial College London, UK; University of Bristol, UK)
Publisher's Version
Article: popl22main-p706-p doi:10.1145/3498723
|
| |
Wu, Zhilin |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Solving String Constraints ..."
Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables
Taolue Chen, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu
(Birkbeck University of London, UK; Royal Holloway University of London, UK; Tsinghua University, China; Institute of Software at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; TU Kaiserslautern, Germany; MPI-SWS, Germany; Uppsala University, Sweden)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p350-p doi:10.1145/3498707
|
| |
Xie, Ningning
|
Proc. ACM Program. Lang., vol. 6, issue POPL: "Staging with Class: A Specification ..."
Staging with Class: A Specification for Typed Template Haskell
Ningning Xie, Matthew Pickering, Andres Löh, Nicolas Wu, Jeremy Yallop, and Meng Wang
(University of Cambridge, UK; Well-Typed LLP, UK; Imperial College London, UK; University of Bristol, UK)
Publisher's Version
Article: popl22main-p706-p doi:10.1145/3498723
|
| |
Yallop, Jeremy
|
Proc. ACM Program. Lang., vol. 6, issue POPL: "Staging with Class: A Specification ..."
Staging with Class: A Specification for Typed Template Haskell
Ningning Xie, Matthew Pickering, Andres Löh, Nicolas Wu, Jeremy Yallop, and Meng Wang
(University of Cambridge, UK; Well-Typed LLP, UK; Imperial College London, UK; University of Bristol, UK)
Publisher's Version
Article: popl22main-p706-p doi:10.1145/3498723
|
| |
Yang, Rem |
Proc. ACM Program. Lang., vol. 6, issue POPL: "A Dual Number Abstraction ..."
A Dual Number Abstraction for Static Analysis of Clarke Jacobians
Jacob Laurel, Rem Yang, Gagandeep Singh, and Sasa Misailovic
(University of Illinois at Urbana-Champaign, USA; VMware, USA)
Publisher's Version
Article: popl22main-p542-p doi:10.1145/3498718
|
| |
Ye, Qianchuan |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Oblivious Algebraic Data Types ..."
Oblivious Algebraic Data Types
Qianchuan Ye and Benjamin Delaware
(Purdue University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p429-p doi:10.1145/3498713
|
| |
Yu, Hongtao |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Profile Inference Revisited ..."
Profile Inference Revisited
Wenlei He, Julián Mestre, Sergey Pupyrev, Lei Wang, and Hongtao Yu
(Facebook, USA; University of Sydney, Australia)
Publisher's Version
Article: popl22main-p431-p doi:10.1145/3498714
|
| |
Yuan, Charles |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Twist: Sound Reasoning for ..."
Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs
Charles Yuan, Christopher McNally, and Michael Carbin
(Massachusetts Institute of Technology, USA)
Publisher's Version
Published Artifact
Archive submitted (690 kB)
Artifacts Available
Artifacts Reusable
Article: popl22main-p167-p doi:10.1145/3498691
|
| |
Zamdzhiev, Vladimir
|
Proc. ACM Program. Lang., vol. 6, issue POPL: "Semantics for Variational ..."
Semantics for Variational Quantum Programming
Xiaodong Jia, Andre Kornell, Bert Lindenhovius, Michael Mislove, and Vladimir Zamdzhiev
(Hunan University, China; Tulane University, USA; JKU Linz, Austria; Inria, France)
Publisher's Version
Article: popl22main-p149-p doi:10.1145/3498687
|
| |
Zetzsche, Georg |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Context-Bounded Verification ..."
Context-Bounded Verification of Thread Pools
Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche
(MPI-SWS, Germany)
Publisher's Version
Article: popl22main-p90-p doi:10.1145/3498678
|
| |
Zhang, Cheng |
Proc. ACM Program. Lang., vol. 6, issue POPL: "On Incorrectness Logic and ..."
On Incorrectness Logic and Kleene Algebra with Top and Tests
Cheng Zhang, Arthur Azevedo de Amorim, and Marco Gaboardi
(Boston University, USA)
Publisher's Version
Article: popl22main-p160-p doi:10.1145/3498690
|
| |
Zhang, Ling |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Verified Compilation of C ..."
Verified Compilation of C Programs with a Nominal Memory Model
Yuting Wang, Ling Zhang, Zhong Shao, and Jérémie Koenig
(Shanghai Jiao Tong University, China; Yale University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p143-p doi:10.1145/3498686
|
| |
Zhang, Qirun |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Efficient Algorithms for Dynamic ..."
Efficient Algorithms for Dynamic Bidirected Dyck-Reachability
Yuanbo Li, Kris Satya, and Qirun Zhang
(Georgia Institute of Technology, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p725-p doi:10.1145/3498724
|
| |
Zhang, Yihong |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Relational E-matching ..."
Relational E-matching
Yihong Zhang, Yisu Remy Wang, Max Willsey, and Zachary Tatlock
(University of Washington, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: popl22main-p244-p doi:10.1145/3498696
|
| |
Zhang, Yizhou |
Proc. ACM Program. Lang., vol. 6, issue POPL: "Reasoning about “Reasoning ..."
Reasoning about “Reasoning about Reasoning”: Semantics and Contextual Equivalence for Probabilistic Programs with Nested Queries and Recursion
Yizhou Zhang and Nada Amin
(University of Waterloo, Canada; Harvard University, USA)
Publisher's Version
Article: popl22main-p66-p doi:10.1145/3498677
|