POPL 2018

66 papers

1. A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runST · Amin Timany, Léo Stefanesco, Morten Krogh-Jespersen, Lars Birkedal
2. A new proof rule for almost-sure termination · Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, Joost-Pieter Katoen
3. A practical construction for decomposing numerical abstract domains · Gagandeep Singh, Markus Püschel, Martin T. Vechev
4. A principled approach to ornamentation in ML · Thomas Williams, Didier Rémy
5. Algorithmic analysis of termination problems for quantum programs · Yangjia Li, Mingsheng Ying
6. Alone together: compositional reasoning and inference for weak isolation · Gowtham Kaki, Kartik Nagar, Mahsa Najafzadeh, Suresh Jagannathan
7. An axiomatic basis for bidirectional programming · Hsiang-Shang Ko, Zhenjiang Hu
8. Analytical modeling of cache behavior for affine programs · Wenlei Bao, Sriram Krishnamoorthy, Louis-Noël Pouchet, P. Sadayappan
9. Automated lemma synthesis in symbolic-heap separation logic · Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, Wei-Ngan Chin
10. Bonsai: synthesis-based reasoning for type systems · Kartik Chandra, Rastislav Bodík
11. Collapsing towers of interpreters · Nada Amin, Tiark Rompf
12. Correctness of speculative optimizations with dynamic deoptimization · Olivier Flückiger, Gabriel Scherer, Ming-Ho Yee, Aviral Goel, Amal Ahmed, Jan Vitek
13. Data-centric dynamic partial order reduction · Marek Chalupa, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, Kapil Vaidya
14. Decidability of conversion for type theory in type theory · Andreas Abel, Joakim Öhman, Andrea Vezzosi
15. Denotational validation of higher-order Bayesian inference · Adam Scibior, Ohad Kammar, Matthijs Vákár, Sam Staton, Hongseok Yang, Yufei Cai + 4 more
16. Effective stateless model checking for C/C++ concurrency · Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, Viktor Vafeiadis
17. Foundations for natural proofs and quantifier instantiation · Christof Löding, P. Madhusudan, Lucas Peña
18. Generating good generators for inductive relations · Leonidas Lampropoulos, Zoe Paraskevopoulou, Benjamin C. Pierce
19. Go with the flow: compositional abstractions for concurrent data structures · Siddharth Krishna, Dennis E. Shasha, Thomas Wies
20. Handle with care: relational interpretation of algebraic effects and handlers · Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, Filip Sieczkowski
21. Handling fibred algebraic effects · Danel Ahman
22. Higher-order constrained horn clauses for verification · Toby Cathcart Burn, C.-H. Luke Ong, Steven J. Ramsay
23. Inference of static semantics for incomplete C programs · Leandro T. C. Melo, Rodrigo Geraldo Ribeiro, Marcus R. de Araújo, Fernando Magno Quintão Pereira
24. Intrinsically-typed definitional interpreters for imperative languages · Casper Bach Poulsen, Arjen Rouvoet, Andrew Tolmach, Robbert Krebbers, Eelco Visser
25. JaVerT: JavaScript verification toolchain · José Fragoso Santos, Petar Maksimovic, Daiva Naudziuniene, Thomas Wood, Philippa Gardner
26. Jones-optimal partial evaluation by specialization-safe normalization · Matt Brown, Jens Palsberg
27. Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs · Sheshansh Agrawal, Krishnendu Chatterjee, Petr Novotný
28. Linear Haskell: practical linearity in a higher-order polymorphic language · Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, Arnaud Spiwack
29. Linearity in higher-order recursion schemes · Pierre Clairambault, Charles Grellois, Andrzej S. Murawski
30. Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming · Thomas Ehrhard, Michele Pagani, Christine Tasson
31. Migrating gradual types · John Peter Campora III, Sheng Chen, Martin Erwig, Eric Walkingshaw
32. Monadic refinements for relational cost analysis · Ivan Radicek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Florian Zuleger
33. Non-linear reasoning for invariant synthesis · Zachary Kincaid, John Cyphert, Jason Breck, Thomas W. Reps
34. On automatically proving the correctness of math.h implementations · Wonyeol Lee, Rahul Sharma, Alex Aiken
35. 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 + 1 more
36. Optimal Dyck reachability for data-dependence and alias analysis · Krishnendu Chatterjee, Bhavya Choudhary, Andreas Pavlogiannis
37. Parametricity versus the universal type · Dominique Devriese, Marco Patrignani, Frank Piessens
38. Polyadic approximations, fibrations and intersection types · Damiano Mazza, Luc Pellissier, Pierre Vial
39. Program synthesis using abstraction refinement · Xinyu Wang, Isil Dillig, Rishabh Singh
40. Programming and proving with distributed protocols · Ilya Sergey, James R. Wilcox, Zachary Tatlock
41. Progress of concurrent objects with partial methods · Hongjin Liang, Xinyu Feng
42. Proving expected sensitivity of probabilistic programs · Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
43. Recalling a witness: foundations and applications of monotonic state · Danel Ahman, Cédric Fournet, Catalin Hritcu, Kenji Maillard, Aseem Rastogi, Nikhil Swamy
44. Reducing liveness to safety in first-order logic · Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, Sharon Shoham
45. Refinement reflection: complete verification with SMT · Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler + 1 more
46. Relatively complete refinement type system for verification of higher-order non-deterministic programs · Hiroshi Unno, Yuki Satake, Tachio Terauchi
47. RustBelt: securing the foundations of the rust programming language · Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer
48. Safety and conservativity of definitions in HOL and Isabelle/HOL · Ondrej Kuncar, Andrei Popescu
49. Simplicitly: foundations and applications of implicit function types · Martin Odersky, Olivier Blanvillain, Fengyun Liu, Aggelos Biboudis, Heather Miller, Sandro Stucki
50. Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8 · Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, Peter Sewell
51. Soft contract verification for higher-order stateful programs · Phuc C. Nguyen, Thomas Gilray, Sam Tobin-Hochstadt, David Van Horn
52. Sound, complete, and tractable linearizability monitoring for concurrent collections · Michael Emmi, Constantin Enea
53. Strategy synthesis for linear arithmetic games · Azadeh Farzan, Zachary Kincaid
54. String constraints with concatenation and transducers solved efficiently · Lukás Holík, Petr Janku, Anthony W. Lin, Philipp Rümmer, Tomás Vojnar
55. Symbolic types for lenient symbolic execution · Stephen Chang, Alex Knauth, Emina Torlak
56. Synthesizing bijective lenses · Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, Steve Zdancewic
57. Synthesizing coupling proofs of differential privacy · Aws Albarghouthi, Justin Hsu
58. Transactions in relaxed memory architectures · Brijesh Dongol, Radha Jagadeesan, James Riely
59. Type-preserving CPS translation of Σ and Π types is not not possible · William J. Bowman, Youyou Cong, Nick Rioux, Amal Ahmed
60. Unifying analytic and statically-typed quasiquotes · Lionel Parreaux, Antoine Voizard, Amir Shaikhha, Christoph E. Koch
61. Univalent higher categories via complete Semi-Segal types · Paolo Capriotti, Nicolai Kraus
62. Up-to techniques using sized types · Nils Anders Danielsson
63. Verifying equivalence of database-driven applications · Yuepeng Wang, Isil Dillig, Shuvendu K. Lahiri, William R. Cook
64. WebRelate: integrating web data with spreadsheets using examples · Jeevana Priya Inala, Rishabh Singh
65. What is decidable about string constraints with the ReplaceAll function · Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, Zhilin Wu
66. Why is random testing effective for partition tolerance bugs? · Rupak Majumdar, Filip Niksic