Links to accepted papers for the 45th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2018). Pull requests welcome!
(Similar pages are available for POPL 2017, 2016, 2015, 2014, and 2013, ICFP (2016, 2015, 2014, 2013, 2012) and PLDI 2014.)
Note: if you are editing this repository, please remember to use the Markdown syntax for hard line breaks, namely two spaces at the end of the line.
A Logical Relation for Monadic Encapsulation of State: Proving contextual equivalences in the presence of runST
Amin Timany, Leo Stefanesco, Morten Krogh-Jespersen, Lars Birkedal
(print)
A Practical Construction for Decomposing Numerical Abstract Domains
Gagandeep Singh, Markus Püschel, Martin Vechev
(preprint)
A Principled approach to Ornamentation in ML
Thomas Williams, Didier Rémy
(preprint from HAL, extended preprint from HAL, website)
A new proof rule for almost-sure termination
Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, Joost-Pieter Katoen
(preprint from arXiv)
Algorithmic Analysis of Termination Problems for Quantum Programs
Yangjia Li, Mingsheng Ying
Alone Together: Compositional Reasoning and Inference for Weak Isolation
Gowtham Kaki, Mahsa Najafzadeh, Kartik Nagar, Suresh Jagannathan
(preprint from arXiv)
An Axiomatic Basis for Bidirectional Programming
Hsiang-Shang ‘Josh’ Ko, Zhenjiang Hu
(preprint,
agda code,
website)
Analytical Modeling of Cache Behavior and Vulnerability Optimization for Affine Programs
Wenlei Bao, Sriram Krishnamoorthy, Louis-Noel Pouchet, P. (Saday) Sadayappan
Automated Lemma Synthesis in Symbolic-Heap Separation Logic
Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, Wei Ngan Chin
(preprint from arXiv)
Bonsai: Synthesis-Based Reasoning for Type Systems
Kartik Chandra, Rastislav Bodik
(preprint from arXiv)
Collapsing Towers of Interpreters
Nada Amin, Tiark Rompf
(print, code)
Correctness of Speculative Optimizations with Dynamic Deoptimization
Olivier Fluckiger, Gabriel Scherer, Ming-Ho Yee, Aviral Goel, Amal Ahmed, Jan Vitek
(preprint from arXiv)
Data-centric Dynamic Partial Order Reduction
Krishnendu Chatterjee, Marek Chalupa, Andreas Pavlogiannis, Nishant Sinha, Kapil Vaidya
(preprint from arXiv)
Decidability of Conversion for Type Theory in Type Theory
Andreas Abel, Andrea Vezzosi, Joakim Öhman
(print, agda code)
Denotational validation of higher-order Bayesian inference
Adam Ścibior, Ohad Kammar, Matthijs Vákár, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Sean Moss, Chris Heunen, Zoubin Ghahramani
(preprint from arXiv)
Effective Stateless Model Checking for C/C++ Concurrency
Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, Viktor Vafeiadis
(preprint, website)
Foundations for Natural Proofs and Quantifier Instantiation
Christof Löding, P. Madhusudan, Lucas Peña
(preprint)
Generating Good Generators for Inductive Relations
Leonidas Lampropoulos, Zoe Paraskevopoulou, Benjamin C. Pierce
(preprint)
Go with the Flow: Compositional Abstractions for Concurrent Data Structures
Siddharth Krishna, Dennis Shasha, Thomas Wies
(preprint from arXiv)
Handle with Care: Relational Interpretation of Algebraic Effects and Handlers
Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, Filip Sieczkowski
(preprint,
coq development)
Handling fibred algebraic effects
Danel Ahman
(preprint,
agda code)
Higher-Order Constrained Horn Clauses for Verification
Toby Cathcart Burn, C.-H. Luke Ong, Steven Ramsay
(preprint from arXiv)
Inference of Static Semantics for Incomplete C Programs
Leandro T. C. Melo, Rodrigo Geraldo Ribeiro, Marcus Rodrigues de Araújo, Fernando Magno Quintão Pereira
(preprint)
Intrinsically-Typed Definitional Interpreters for Imperative Languages
Casper Bach Poulsen, Arjen Rouvoet, Andrew Tolmach, Robbert Krebbers, Eelco Visser
(preprint,
agda code
)
JaVerT: JavaScript Verification Toolchain
José Fragoso Santos, Philippa Gardner, Petar Maksimović, Daiva Naudziuniene, Thomas Wood
(preprint)
Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs
Sheshansh Agrawal, Krishnendu Chatterjee, Petr Novotny
(preprint from arXiv)
Linear Haskell: practical linearity in a higher-order polymorphic language
Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, Arnaud Spiwack
(preprint from arXiv)
Linearity in Higher-Order Recursion Schemes
Pierre Clairambault, Charles Grellois, Andrzej Murawski
(preprint)
Measurable cones and stable, measurable functions
Thomas Ehrhard, Michele Pagani, Christine Tasson
(preprint from arXiv)
Migrating Gradual Types
John Peter Campora III, Sheng Chen, Martin Erwig, Eric Walkingshaw
(preprint)
Monadic refinements for relational cost analysis
Ivan Radicek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Florian Zuleger
(preprint)
Non-Linear Reasoning For Invariant Synthesis
Jason Breck, John Cyphert, Zachary Kincaid, Thomas Reps
(preprint)
On Automatically Proving the Correctness of math.h Implementations
Wonyeol Lee, Rahul Sharma, Alex Aiken
(preprint)
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, Yoni Zohar
(preprint)
Optimal Dyck Reachability for Data-dependence and Alias Analysis
Krishnendu Chatterjee, Andreas Pavlogiannis, Bhavya Choudhary
(preprint)
Parametricity versus the Universal Type
Dominique Devriese, Marco Patrignani, Frank Piessens
(preprint)
Polyadic Approximations, Fibrations and Intersection Types
Damiano Mazza, Luc Pellissier, Pierre Vial
(preprint)
Program Synthesis using Abstraction Refinement
Xinyu Wang, Isil Dillig, Rishabh Singh
(preprint from arXiv)
Programming and Proving with Distributed Protocols
Ilya Sergey, James R. Wilcox, Zachary Tatlock
(preprint)
Progress of Concurrent Objects with Partial Methods
Hongjin Liang, Xinyu Feng
Proving expected sensitivity of probabilistic programs
Gilles Barthe, Thomas Espitau, Benjamin Gregoire, Justin Hsu, Pierre-Yves Strub
(preprint from arXiv)
Recalling a Witness: Foundations and Applications of Monotonic State
Danel Ahman, Cédric Fournet, Cătălin Hriţcu, Kenji Maillard, Aseem Rastogi, Nikhil Swamy
(preprint from arXiv)
Reducing Liveness to Safety in First-Order Logic
Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, Sharon Shoham
(preprint, website)
Refinement Reflection: Complete Verification with SMT
Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan Scott, Ryan R. Newton, Philip Wadler, Ranjit Jhala
(preprint from arXiv)
Relatively Complete Refinement Type System for Verification of Higher-Order Non-Deterministic Programs
Hiroshi Unno, Yuki Satake, Tachio Terauchi
RustBelt: Securing the Foundations of the Rust Programming Language
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer
(preprint)
Safety and Conservativity of Definitions in HOL and Isabelle/HOL
Ondřej Kunčar, Andrei Popescu
(preprint)
Simplicitly: Foundations and Applications of Implicit Function Types
Martin Odersky, Olivier Blanvillain, Fengyun Liu, Aggelos Biboudis, Heather Miller, Sandro Stucki
(preprint)
Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8
Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, Peter Sewell
(draft, website)
Soft Contract Verification for Higher-order Stateful Programs
Phúc C. Nguyễn, Thomas Gilray, Sam Tobin-Hochstadt, David Van Horn
(preprint from arXiv)
Sound, Complete, and Tractable Linearizability Monitoring for Concurrent Collections
Michael Emmi, Constantin Enea
(preprint)
Strategy Synthesis for Linear Arithmetic Games
Azadeh Farzan, Zachary Kincaid
(preprint)
String Constraints with Concatenation and Transducers Solved Efficiently
Lukas Holik, Anthony Widjaja Lin, Petr Janku, Philipp Ruemmer, Tomas Vojnar
(technical report)
Symbolic Types for Lenient Symbolic Execution
Stephen Chang, Alex Knauth, Emina Torlak
(draft, website)
Synthesizing Bijective Lenses
Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, Steve Zdancewic
(preprint from arXiv)
Synthesizing Coupling Proofs of Differential Privacy
Aws Albarghouthi, Justin Hsu
(preprint from arXiv)
Transactions in Relaxed Memory Architectures
Brijesh Dongol, Radha Jagadeesan, James Riely
(preprint)
Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible
William J. Bowman, Youyou Cong, Nick Rioux, Amal Ahmed
(draft, website)
Typed and Jones Optimal Self-Applicable Partial Evaluation
Matt Brown, Jens Palsberg
Unifying Analytic and Statically-Typed Quasiquotes
Lionel Parreaux, Antoine Voizard, Amir Shaikhha, Christoph E. Koch
(preprint)
Univalent Higher Categories via Complete Semi-Segal Types
Paolo Capriotti, Nicolai Kraus
(preprint from arXiv)
Up-to Techniques Using Sized Types
Nils Anders Danielsson
(draft)
Verifying Equivalence of Database-Driven Applications
Yuepeng Wang, Isil Dillig, Shuvendu K. Lahiri, William Cook
(preprint from arXiv)
WebRelate: Integrating Web Data with Spreadsheets using Examples
Jeevana Priya Inala, Rishabh Singh
(preprint from arXiv)
What's Decidable About String Constraints with ReplaceAll Function?
Taolue Chen, Yan Chen, Matthew Hague, Anthony Widjaja Lin, Zhilin Wu
(preprint from arXiv)
Why is Random Testing Effective for Partition Tolerance Bugs?
Rupak Majumdar, Filip Niksic
(preprint)