POPL – Journal Issue

Frontmatter

Strings

Synthesizing Bijective Lenses
Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve Zdancewic
(Princeton University, USA; Tufts University, USA; University of Pennsylvania, USA)


Artifacts Functional

WebRelate: Integrating Web Data with Spreadsheets using Examples
Jeevana Priya Inala and Rishabh Singh
(Massachusetts Institute of Technology, USA; Microsoft Research, USA)


Artifacts Functional

String Constraints with Concatenation and Transducers Solved Efficiently
Lukáš Holík, Petr Janků, Anthony W. Lin, Philipp Rümmer, and Tomáš Vojnar
(Brno University of Technology, Czechia; University of Oxford, UK; Uppsala University, Sweden)


Artifacts Functional

Types and Effects 1

Linear Haskell: Practical Linearity in a Higher-Order Polymorphic Language
Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, and Arnaud Spiwack
(University of Gothenburg, Sweden; Tweag I/O, France; Indiana University, USA; Microsoft Research, UK)


Artifacts Functional

Handle with Care: Relational Interpretation of Algebraic Effects and Handlers
Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski
(University of Wrocław, Poland)


Artifacts Functional

Verification

Automated Lemma Synthesis in Symbolic-Heap Separation Logic
Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin
(National University of Singapore, Singapore)


Artifacts Functional

Foundations for Natural Proofs and Quantifier Instantiation
Christof Löding, P. Madhusudan, and Lucas Peña
(RWTH Aachen University, Germany; University of Illinois at Urbana-Champaign, USA)


Artifacts Functional

Higher-Order Constrained Horn Clauses for Verification
Toby Cathcart Burn, C.-H. Luke Ong, and Steven J. Ramsay
(University of Oxford, UK; University of Bristol, UK)


Artifacts Functional

Interpretation and Evaluation

Unifying Analytic and Statically-Typed Quasiquotes
Lionel Parreaux, Antoine Voizard, Amir Shaikhha, and Christoph E. Koch
(EPFL, Switzerland; University of Pennsylvania, USA)


Artifacts Functional

Jones-Optimal Partial Evaluation by Specialization-Safe Normalization
Matt Brown and Jens Palsberg
(University of California at Los Angeles, USA)


Artifacts Functional

Migrating Gradual Types
John Peter Campora, Sheng Chen, Martin Erwig, and Eric Walkingshaw
(University of Louisiana at Lafayette, USA; Oregon State University, USA)


Artifacts Functional

Intrinsically-Typed Definitional Interpreters for Imperative Languages
Casper Bach Poulsen, Arjen Rouvoet, Andrew Tolmach, Robbert Krebbers, and Eelco Visser
(Delft University of Technology, Netherlands; Portland State University, USA)


Artifacts Functional

Memory and Concurrency

Effective Stateless Model Checking for C/C++ Concurrency
Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, and Viktor Vafeiadis
(National Technical University of Athens, Greece; Tel Aviv University, Israel; Uppsala University, Sweden; MPI-SWS, Germany)


Artifacts Functional

Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8
Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell
(University of Cambridge, UK; ARM, UK; University of St. Andrews, UK)


Artifacts Functional

Types

A Principled Approach to Ornamentation in ML
Thomas Williams and Didier Rémy
(Inria, France)


Artifacts Functional

Decidability of Conversion for Type Theory in Type Theory
Andreas Abel, Joakim Öhman, and Andrea Vezzosi
(University of Gothenburg, Sweden; IMDEA Software Institute, Spain; Chalmers University of Technology, Sweden)


Artifacts Functional

Consistency

Reducing Liveness to Safety in First-Order Logic
Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, and Sharon Shoham
(Tel Aviv University, Israel; University of Freiburg, Germany; University of California at Los Angeles, USA)


Artifacts Functional

Programming and Proving with Distributed Protocols
Ilya Sergey, James R. Wilcox, and Zachary Tatlock
(University College London, UK; University of Washington, USA)


Artifacts Functional

Types and Effects 2

Inference of Static Semantics for Incomplete C Programs
Leandro T. C. Melo, Rodrigo G. Ribeiro, Marcus R. de Araújo, and Fernando Magno Quintão Pereira
(Federal University of Minas Gerais, Brazil; Federal University of Ouro Preto, Brazil)


Artifacts Functional

Optimal Dyck Reachability for Data-Dependence and Alias Analysis
Krishnendu Chatterjee, Bhavya Choudhary, and Andreas Pavlogiannis
(IST Austria, Austria; IIT Bombay, India)


Artifacts Functional

Termination

Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs
Sheshansh Agrawal, Krishnendu Chatterjee, and Petr Novotný
(IIT Bombay, India; IST Austria, Austria)


Artifacts Functional

Outside the Box

Symbolic Types for Lenient Symbolic Execution
Stephen Chang, Alex Knauth, and Emina Torlak
(Northeastern University, USA; University of Washington, USA)


Artifacts Functional

Language Design

An Axiomatic Basis for Bidirectional Programming
Hsiang-Shang Ko and Zhenjiang Hu
(National Institute of Informatics, Japan)


Artifacts Functional

Simplicitly: Foundations and Applications of Implicit Function Types
Martin Odersky, Olivier Blanvillain, Fengyun Liu, Aggelos Biboudis, Heather Miller, and Sandro Stucki
(EPFL, Switzerland; Northeastern University, USA)


Artifacts Functional

Dependent Types

Up-to Techniques using Sized Types
Nils Anders Danielsson
(University of Gothenburg, Sweden; Chalmers University of Technology, Sweden)


Artifacts Functional

Univalent Higher Categories via Complete Semi-Segal Types
Paolo Capriotti and Nicolai Kraus
(University of Nottingham, UK)


Artifacts Functional

Testing and Verification

Generating Good Generators for Inductive Relations
Leonidas Lampropoulos, Zoe Paraskevopoulou, and Benjamin C. Pierce
(University of Pennsylvania, USA; Princeton University, USA)


Artifacts Functional

Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts
Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, and Yoni Zohar
(Tel Aviv University, Israel; VMware, USA; Stanford University, USA)


Artifacts Functional

Dynamic Languages

JaVerT: JavaScript Verification Toolchain
José Fragoso Santos, Petar Maksimović, Daiva Naudžiūnienė, Thomas Wood, and Philippa Gardner
(Imperial College London, UK; Mathematical Institute SASA, Serbia)


Artifacts Functional

Soft Contract Verification for Higher-Order Stateful Programs
Phúc C. Nguyễn, Thomas Gilray, Sam Tobin-Hochstadt, and David Van Horn
(University of Maryland, USA; Indiana University, USA)


Artifacts Functional

Collapsing Towers of Interpreters
Nada Amin and Tiark Rompf
(University of Cambridge, UK; Purdue University, USA)


Artifacts Functional

Program Analysis

Refinement Reflection: Complete Verification with SMT
Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, and Ranjit Jhala
(University of Maryland, USA; University of California at San Diego, USA; Indiana University, USA; University of Edinburgh, UK; Input Output HK, UK)


Artifacts Functional

Non-linear Reasoning for Invariant Synthesis
Zachary Kincaid, John Cyphert, Jason Breck, and Thomas Reps
(Princeton University, USA; University of Wisconsin-Madison, USA; GrammaTech, USA)


Artifacts Functional

A Practical Construction for Decomposing Numerical Abstract Domains
Gagandeep Singh, Markus Püschel, and Martin Vechev
(ETH Zurich, Switzerland)


Artifacts Functional

Probability

Proving Expected Sensitivity of Probabilistic Programs
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub
(IMDEA Software Institute, Spain; UPMC, France; Inria, France; University College London, UK; École Polytechnique, France)


Artifacts Functional

Synthesis

Strategy Synthesis for Linear Arithmetic Games
Azadeh Farzan and Zachary Kincaid
(University of Toronto, Canada; Princeton University, USA)


Artifacts Functional

Bonsai: Synthesis-Based Reasoning for Type Systems
Kartik Chandra and Rastislav Bodik
(Henry M. Gunn High School, USA; Stanford University, USA; University of Washington, USA)


Artifacts Functional

Types for State

A Logical Relation for Monadic Encapsulation of State: Proving Contextual Equivalences in the Presence of runST
Amin Timany, Léo Stefanesco, Morten Krogh-Jespersen, and Lars Birkedal
(KU Leuven, Belgium; IRIF, France; CNRS, France; University of Paris Diderot, France; Aarhus University, Denmark)


Artifacts Functional

Recalling a Witness: Foundations and Applications of Monotonic State
Danel Ahman, Cédric Fournet, Cătălin Hriţcu, Kenji Maillard, Aseem Rastogi, and Nikhil Swamy
(Inria, France; Microsoft Research, UK; ENS Paris, France; Microsoft Research, India; Microsoft Research, USA)


Artifacts Functional

RustBelt: Securing the Foundations of the Rust Programming Language
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer
(MPI-SWS, Germany; Delft University of Technology, Netherlands)


Artifacts Functional

proc time: 0.1