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
(preprint)
A Practical Construction for Decomposing Numerical Abstract Domains
Gagandeep Singh, Markus Püschel, Martin Vechev
A Principled approach to Ornamentation in ML
Thomas Williams, Didier Rémy
(draft)
A new proof rule for almost-sure termination
Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, Joost-Pieter Katoen
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
(draft)
Complete Verification with SMT
Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan Scott, Ryan R. Newton, Philip Wadler, Ranjit Jhala
(preprint)
Correctness of Speculative Optimizations with Dynamic Deoptimization
Olivier Fluckiger, Gabriel Scherer, Ming-Ho Yee, Aviral Goel, Amal Ahmed, Jan Vitek
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
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
Effective Stateless Model Checking for C/C++ Concurrency
Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, Viktor Vafeiadis
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
Handle with Care: Relational Interpretation of Algebraic Effects and Handlers
Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, Filip Sieczkowski
Handling fibred algebraic effects
Danel Ahman
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
Intrinsically-Typed Definitional Interpreters for Imperative Languages
Casper Bach Poulsen, Arjen Rouvoet, Andrew Tolmach, Robbert Krebbers, Eelco Visser
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
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
Measurable cones and stable, measurable functions
Thomas Ehrhard, Michele Pagani, Christine Tasson
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
Non-Linear Reasoning For Invariant Synthesis
Jason Breck, John Cyphert, Zachary Kincaid, Thomas Reps
On Automatically Proving the Correctness of math.h Implementations
Wonyeol Lee, Rahul Sharma, Alex Aiken
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
Optimal Dyck Reachability for Data-dependence and Alias Analysis
Krishnendu Chatterjee, Andreas Pavlogiannis, Bhavya Choudhary
Parametricity versus the Universal Type
Dominique Devriese, Marco Patrignani, Frank Piessens
Program Synthesis using Abstraction Refinement
Xinyu Wang, Isil Dillig, Rishabh Singh
Programming and Proving with Distributed Protocols
Ilya Sergey, James R. Wilcox, Zachary Tatlock
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
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)
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)
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
Sound, Complete, and Tractable Linearizability Monitoring for Concurrent Collections
Michael Emmi, Constantin Enea
Strategy Synthesis for Linear Arithmetic Games
Azadeh Farzan, Zachary Kincaid
String Constraints with Concatenation and Transducers Solved Efficiently
Lukas Holik, Anthony Widjaja Lin, Petr Janku, Philipp Ruemmer, Tomas Vojnar
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
Synthesizing Coupling Proofs of Differential Privacy
Aws Albarghouthi, Justin Hsu
Transactions in Relaxed Memory Architectures
Brijesh Dongol, Radha Jagadeesan, James Riely
Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible
William J. Bowman, Youyou Cong, Nick Rioux, Amal Ahmed
(draft, website)
Unifying Analytic and Statically-Typed Quasiquotes
Lionel Parreaux, Antoine Voizard, Amir Shaikhha, Christoph E. Koch
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
WebRelate: Integrating Web Data with Spreadsheets using Examples
Jeevana Priya Inala, Rishabh Singh
What's Decidable About String Constraints with ReplaceAll Function?
Taolue Chen, Yan Chen, Matthew Hague, Anthony Widjaja Lin, Zhilin Wu
Why is Random Testing Effective for Partition Tolerance Bugs?
Rupak Majumdar, Filip Niksic