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

Proceedings of the ACM on Programming Languages, Volume 3, Number POPL, January 13–19, 2019, Cascais, Portugal

POPL – Journal Issue

Contents - Abstracts - Authors
Title Page

Papers

Higher Inductive Types in Cubical Computational Type Theory
Evan Cavallo and Robert Harper
(Carnegie Mellon University, USA)
Article Search
Constructing Quotient Inductive-Inductive Types
Ambrus Kaposi, András Kovács, and Thorsten Altenkirch
(Eötvös Loránd University, Hungary; University of Nottingham, UK)
Article Search Info Artifacts Available Artifacts Functional
Definitional Proof-Irrelevance without K
Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau
(Inria, France; Chalmers University of Technology, Sweden; University of Gothenburg, Sweden; IRIF, France)
Article Search Artifacts Available Artifacts Reusable
Bisimulation as Path Type for Guarded Recursive Types
Rasmus Ejlers Møgelberg and Niccolò Veltri
(IT University of Copenhagen, Denmark)
Article Search
Abstraction-Safe Effect Handlers via Tunneling
Yizhou Zhang and Andrew C. Myers
(Cornell University, USA)
Article Search
Abstracting Algebraic Effects
Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski
(University of Wrocław, Poland)
Article Search Artifacts Available Artifacts Reusable
Intersection Types and Runtime Errors in the Pi-Calculus
Ugo Dal Lago, Marc de Visme, Damiano Mazza, and Akira Yoshimizu
(University of Bologna, Italy; ENS Lyon, France; CNRS, France; University of Paris 13, France)
Article Search
Principality and Approximation under Dimensional Bound
Andrej Dudenhefner and Jakob Rehof
(TU Dortmund, Germany)
Article Search
Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism with Existentials and Indexed Types
Joshua Dunfield and Neelakantan R. Krishnaswami
(Queen's University, Canada; University of Cambridge, UK)
Article Search
Fully Abstract Module Compilation
Karl Crary
(Carnegie Mellon University, USA)
Preprint Artifacts Available Artifacts Functional
Polymorphic Symmetric Multiple Dispatch with Variance
Gyunghee Park, Jaemin Hong, Guy L. Steele Jr., and Sukyoung Ryu
(KAIST, South Korea; Oracle Labs, USA)
Article Search
Abstracting Extensible Data Types: Or, Rows by Any Other Name
J. Garrett Morris and James McKinna
(University of Kansas, USA; University of Edinburgh, UK)
Article Search
Type-Guided Worst-Case Input Generation
Di Wang and Jan Hoffmann
(Carnegie Mellon University, USA)
Preprint Artifacts Available Artifacts Functional
Live Functional Programming with Typed Holes
Cyrus Omar, Ian Voysey, Ravi Chugh, and Matthew A. Hammer
(University of Chicago, USA; Carnegie Mellon University, USA; University of Colorado Boulder, USA)
Article Search Info Artifacts Available Artifacts Reusable
Gradual Type Theory
Max S. New, Daniel R. Licata, and Amal Ahmed
(Northeastern University, USA; Wesleyan University, USA; Inria, France)
Article Search
Gradual Typing: A New Perspective
Giuseppe Castagna, Victor Lanvin, Tommaso Petrucciani, and Jeremy G. Siek
(CNRS, France; University of Paris Diderot, France; University of Genoa, Italy; Indiana University at Bloomington, USA)
Article Search
Gradual Parametricity, Revisited
Matías Toro, Elizabeth Labrada, and Éric Tanter
(University of Chile, Chile; Inria, France)
Preprint Info Artifacts Available Artifacts Reusable
Dynamic Type Inference for Gradual Hindley–Milner Typing
Yusuke Miyazaki, Taro Sekiyama, and Atsushi Igarashi
(Kyoto University, Japan; National Institute of Informatics, Japan)
Preprint Artifacts Available Artifacts Reusable
StkTokens: Enforcing Well-Bracketed Control Flow and Stack Encapsulation Using Linear Capabilities
Lau Skorstengaard, Dominique Devriese, and Lars Birkedal
(Aarhus University, Denmark; Vrije Universiteit Brussel, Belgium)
Article Search
Modalities, Cohesion, and Information Flow
G. A. Kavvos
(Wesleyan University, USA)
Article Search
Familial Monads and Structural Operational Semantics
Tom Hirschowitz
(Grenoble Alps University, France; Savoie Mont Blanc University, France; CNRS, France; LAMA, France)
Preprint
Bindings as Bounded Natural Functors
Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, and Dmitriy Traytel
(Vrije Universiteit Amsterdam, Netherlands; Middlesex University, UK; ETH Zurich, Switzerland)
Preprint Info Artifacts Available Artifacts Reusable
Categorical Combinatorics of Scheduling and Synchronization in Game Semantics
Paul-André Mellies
(CNRS, France; University of Paris Diderot, France)
Article Search
Better Late Than Never: A Fully-Abstract Semantics for Classical Processes
Wen Kokke, Fabrizio Montesi, and Marco Peressotti
(University of Edinburgh, UK; University of Southern Denmark, Denmark)
Preprint
Diagrammatic Algebra: From Linear to Concurrent Systems
Filippo Bonchi, Joshua Holland, Pawel Sobocinski, Robin Piedeleu, and Fabio Zanasi
(University of Pisa, Italy; University of Southampton, UK; University of Oxford, UK; University College London, UK)
Article Search
Fixpoint Games on Continuous Lattices
Paolo Baldan, Barbara König, Christina Mika-Michalski, and Tommaso Padoan
(University of Padua, Italy; University of Duisburg-Essen, Germany)
Article Search
Two Sides of the Same Coin: Session Types and Game Semantics: A Synchronous Side and an Asynchronous Side
Simon Castellan and Nobuko Yoshida
(Imperial College London, UK)
Article Search
Exceptional Asynchronous Session Types: Session Types without Tiers
Simon Fowler, Sam Lindley, J. Garrett Morris, and Sára Decova
(University of Edinburgh, UK; University of Kansas, USA)
Preprint Artifacts Available Artifacts Reusable
Distributed Programming using Role-Parametric Session Types in Go: Statically-Typed Endpoint APIs for Dynamically-Instantiated Communication Structures
David Castro, Raymond Hu, Sung-Shik Jongmans, Nicholas Ng, and Nobuko Yoshida
(Imperial College London, UK; Open University of the Netherlands, Netherlands)
Article Search Artifacts Available Artifacts Reusable
Less Is More: Multiparty Session Types Revisited
Alceste Scalas and Nobuko Yoshida
(Imperial College London, UK)
Preprint Info Artifacts Available Artifacts Reusable
Quantitative Robustness Analysis of Quantum Programs
Shih-Han Hung, Kesha Hietala, Shaopeng Zhu, Mingsheng Ying, Michael Hicks, and Xiaodi Wu
(University of Maryland, USA; University of Technology Sydney, Australia)
Preprint
Game Semantics for Quantum Programming
Pierre Clairambault, Marc De Visme, and Glynn Winskel
(CNRS, France; ENS Lyon, France; University of Cambridge, UK)
Article Search
Quantum Relational Hoare Logic
Dominique Unruh
(University of Tartu, Estonia)
Preprint Artifacts Available Artifacts Reusable
Quantitative Separation Logic: A Logic for Reasoning about Probabilistic Pointer Programs
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll
(RWTH Aachen University, Germany)
Article Search Info
Probabilistic Programming with Densities in SlicStan: Efficient, Flexible, and Deterministic
Maria I. Gorinova, Andrew D. Gordon, and Charles Sutton
(University of Edinburgh, UK; Microsoft Research, UK; Google Brain, USA)
Preprint
A Domain Theory for Statistical Probabilistic Programming
Matthijs Vákár, Ohad Kammar, and Sam Staton
(University of Oxford, UK)
Article Search
Bayesian Synthesis of Probabilistic Programs for Automatic Data Modeling
Feras A. Saad, Marco F. Cusumano-Towner, Ulrich Schaechtle, Martin C. Rinard, and Vikash K. Mansinghka
(Massachusetts Institute of Technology, USA)
Preprint Artifacts Available Artifacts Functional
Formal Verification of Higher-Order Probabilistic Programs: Reasoning about Approximation, Convergence, Bayesian Inference, and Optimization
Tetsuya Sato, Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Justin Hsu
(SUNY Buffalo, USA; IMDEA Software Institute, Spain; MPI-SWS, Germany; University of Wisconsin-Madison, USA)
Article Search
Trace Abstraction Modulo Probability
Calvin Smith, Justin Hsu, and Aws Albarghouthi
(University of Wisconsin-Madison, USA)
Article Search
code2vec: Learning Distributed Representations of Code
Uri Alon, Meital Zilberstein, Omer Levy, and Eran Yahav
(Technion, Israel; Facebook AI Research, USA)
Preprint Info Artifacts Available Artifacts Reusable
An Abstract Domain for Certifying Neural Networks
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev
(ETH Zurich, Switzerland)
Preprint Info Artifacts Available Artifacts Functional
A²I: Abstract² Interpretation
Patrick Cousot, Roberto Giacobazzi, and Francesco Ranzato
(New York University, USA; University of Verona, Italy; University of Padua, Italy)
Article Search
Concerto: A Framework for Combined Concrete and Abstract Interpretation
John Toman and Dan Grossman
(University of Washington, USA)
Article Search Artifacts Available Artifacts Functional
Skeletal Semantics and Their Interpretations
Martin Bodin, Philippa Gardner, Thomas Jensen, and Alan Schmitt
(Imperial College London, UK; Inria, France)
Article Search Info Artifacts Available Artifacts Reusable
Refinement of Path Expressions for Static Analysis
John Cyphert, Jason Breck, Zachary Kincaid, and Thomas Reps
(University of Wisconsin, USA; Princeton University, USA; GrammaTech, USA)
Article Search Artifacts Available Artifacts Reusable
Decidable Verification of Uninterpreted Programs
Umang Mathur, P. Madhusudan, and Mahesh Viswanathan
(University of Illinois at Urbana-Champaign, USA)
Article Search
Inferring Frame Conditions with Static Correlation Analysis
Oana F. Andreescu, Thomas Jensen, Stéphane Lescuyer, and Benoît Montagu
(Internet of Trust, France; Inria, France; Prove & Run, France)
Article Search Artifacts Functional
Context-, Flow-, and Field-Sensitive Data-Flow Analysis using Synchronized Pushdown Systems
Johannes Späth, Karim Ali, and Eric Bodden
(Fraunhofer IEM, Germany; University of Alberta, Canada; University of Paderborn, Germany)
Article Search Artifacts Available Artifacts Reusable
Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations
Taolue Chen, Matthew Hague, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu
(Birkbeck University of London, UK; Royal Holloway University of London, UK; University of Oxford, UK; Uppsala University, Sweden; Institute of Software at Chinese Academy of Sciences, China)
Preprint Artifacts Available Artifacts Reusable
Modular Quantitative Monitoring
Rajeev Alur, Konstantinos Mamouras, and Caleb Stanford
(University of Pennsylvania, USA)
Article Search
Bounded Model Checking of Signal Temporal Logic Properties using Syntactic Separation
Kyungmin Bae and Jia Lee
(POSTECH, South Korea)
Article Search Info Artifacts Available Artifacts Functional
Adventures in Monitorability: From Branching to Linear Time and Back Again
Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen
(Gran Sasso Science Institute, Iceland; Reykjavik University, Iceland; University of Malta, Malta; University of Kiel, Germany)
Preprint
Efficient Parameterized Algorithms for Data Packing
Krishnendu Chatterjee, Amir Kafshdar Goharshady, Nastaran Okati, and Andreas Pavlogiannis
(IST Austria, Austria; Ferdowsi University of Mashhad, Iran; EPFL, Switzerland)
Preprint Info Artifacts Available Artifacts Reusable
Fast and Exact Analysis for LRU Caches
Valentin Touzeau, Claire Maïza, David Monniaux, and Jan Reineke
(Grenoble Alps University, France; CNRS, France; Saarland University, Germany)
Article Search
Closed Forms for Numerical Loops
Zachary Kincaid, Jason Breck, John Cyphert, and Thomas Reps
(Princeton University, USA; University of Wisconsin, USA; GrammaTech, USA)
Article Search Artifacts Available Artifacts Reusable
Efficient Automated Repair of High Floating-Point Errors in Numerical Libraries
Xin Yi, Liqian Chen, Xiaoguang Mao, and Tao Ji
(National University of Defense Technology, China)
Article Search Artifacts Available Artifacts Reusable
A True Positives Theorem for a Static Race Detector
Nikos Gorogiannis, Peter W. O'Hearn, and Ilya Sergey
(Facebook, UK; Middlesex University, UK; University College London, UK; Yale-NUS College, Singapore; National University of Singapore, Singapore)
Preprint Artifacts Available Artifacts Functional
Decoupling Lock-Free Data Structures from Memory Reclamation for Static Analysis
Roland Meyer and Sebastian Wolff
(TU Braunschweig, Germany)
Article Search Info Artifacts Available Artifacts Reusable
Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs
Klaus v. Gleissenthall, Rami Gökhan Kıcı, Alexander Bakst, Deian Stefan, and Ranjit Jhala
(University of California at San Diego, USA)
Article Search Artifacts Available Artifacts Functional
Weak-Consistency Specification via Visibility Relaxation
Michael Emmi and Constantin Enea
(SRI International, n.n.; IRIF, France; University of Paris Diderot, France; CNRS, France)
Article Search
A Calculus for Esterel: If can, can. If no can, no can.
Spencer P. Florence, Shu-Hung You, Jesse A. Tov, and Robert Bruce Findler
(Northwestern University, USA)
Article Search Artifacts Available Artifacts Reusable
An Abstract Stack Based Approach to Verified Compositional Compilation to Machine Code
Yuting Wang, Pierre Wilke, and Zhong Shao
(Yale University, USA)
Article Search Artifacts Functional
A Verified, Efficient Embedding of a Verifiable Assembly Language
Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi, and Nikhil Swamy
(Carnegie Mellon University, USA; Princeton, USA; Microsoft Research, n.n.)
Article Search Artifacts Available Artifacts Functional
A Separation Logic for Concurrent Randomized Programs
Joseph Tassarotti and Robert Harper
(Carnegie Mellon University, USA)
Article Search Artifacts Available Artifacts Reusable
Iron: Managing Obligations in Higher-Order Concurrent Separation Logic
Aleš Bizjak, Daniel Gratzer, Robbert Krebbers, and Lars Birkedal
(Aarhus University, Denmark; Delft University of Technology, Netherlands)
Preprint Artifacts Available Artifacts Reusable
JaVerT 2.0: Compositional Symbolic Execution for JavaScript
José Fragoso Santos, Petar Maksimović, Gabriela Sampaio, and Philippa Gardner
(Imperial College London, UK; Mathematical Institute SASA, Serbia)
Article Search Artifacts Available Artifacts Reusable
Exploring C Semantics and Pointer Provenance
Kayvan Memarian, Victor B. F. Gomes, Brooks Davis, Stephen Kell, Alexander Richardson, Robert N. M. Watson, and Peter Sewell
(University of Cambridge, UK; SRI International, n.n.)
Article Search Info
On Library Correctness under Weak Memory Consistency: Specifying and Verifying Concurrent Libraries under Declarative Consistency Models
Azalea Raad, Marko Doko, Lovro Rožić, Ori Lahav, and Viktor Vafeiadis
(MPI-SWS, Germany; Tel Aviv University, Israel)
Preprint Info Artifacts Available Artifacts Reusable
Bridging the Gap between Programming Languages and Hardware Weak Memory Models
Anton Podkopaev, Ori Lahav, and Viktor Vafeiadis
(St. Petersburg University, Russia; JetBrains Research, Russia; MPI-SWS, Germany; Tel Aviv University, Israel)
Preprint Info Artifacts Available Artifacts Reusable
Grounding Thin-Air Reads with Event Structures
Soham Chakraborty and Viktor Vafeiadis
(MPI-SWS, Germany)
Article Search Info
ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and Peter Sewell
(University of Cambridge, UK; University of Edinburgh, UK; ARM, UK; SRI International, USA)
Article Search Artifacts Functional
Structuring the Synthesis of Heap-Manipulating Programs
Nadia Polikarpova and Ilya Sergey
(University of California at San Diego, USA; Yale-NUS College, Singapore; National University of Singapore, Singapore)
Preprint Info Artifacts Available Artifacts Reusable
FrAngel: Component-Based Synthesis with Control Structures
Kensen Shi, Jacob Steinhardt, and Percy Liang
(Stanford University, USA)
Article Search Info Artifacts Available Artifacts Reusable
Hamsaz: Replication Coordination Analysis and Synthesis
Farzin Houshmand and Mohsen Lesani
(University of California at Riverside, USA)
Article Search
LWeb: Information Flow Security for Multi-tier Web Applications
James Parker, Niki Vazou, and Michael Hicks
(University of Maryland, USA; IMDEA Software Institute, Spain)
Article Search
From Fine- to Coarse-Grained Dynamic Information Flow Control and Back
Marco Vassena, Alejandro Russo, Deepak Garg, Vineet Rajani, and Deian Stefan
(Chalmers University of Technology, Sweden; MPI-SWS, Germany; University of California at San Diego, USA)
Preprint Artifacts Available Artifacts Reusable
CT-Wasm: Type-Driven Secure Cryptography for the Web Ecosystem
Conrad Watt, John Renner, Natalie Popescu, Sunjay Cauligi, and Deian Stefan
(University of Cambridge, UK; University of California at San Diego, USA)
Preprint Info Artifacts Available Artifacts Reusable

proc time: 5.79