POPL 2020

68 papers

1. A language for probabilistically oblivious computation · David Darais, Ian Sweet, Chang Liu, Michael Hicks
2. A probabilistic separation logic · Gilles Barthe, Justin Hsu, Kevin Liao
3. A simple differentiable programming language · Martín Abadi, Gordon D. Plotkin
4. Abstract extensionality: on the properties of incomplete abstract interpretations · Roberto Bruni, Roberto Giacobazzi, Roberta Gori, Isabel Garcia-Contreras, Dusko Pavlovic
5. Abstract interpretation of distributed network control planes · Ryan Beckett, Aarti Gupta, Ratul Mahajan, David Walker
6. Actris: session-type based reasoning in separation logic · Jonas Kastberg Hinrichsen, Jesper Bengtson, Robbert Krebbers
7. Aiming low is harder: induction for lower bounds in probabilistic program verification · Marcel Hark, Benjamin Lucien Kaminski, Jürgen Giesl, Joost-Pieter Katoen
8. Augmented example-based synthesis using relational perturbation properties · Shengwei An, Rishabh Singh, Sasa Misailovic, Roopsha Samanta
9. Backpropagation in the simply typed lambda-calculus with linear negation · Aloïs Brunel, Damiano Mazza, Michele Pagani
10. Binders by day, labels by night: effect instances via lexically scoped handlers · Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, Filip Sieczkowski
11. CompCertM: CompCert with C-assembly linking and lightweight modular verification · Youngju Song, Minki Cho, Dongjoo Kim, Yonghyun Kim, Jeehoon Kang, Chung-Kil Hur
12. Complexity and information in invariant inference · Yotam M. Y. Feldman, Neil Immerman, Mooly Sagiv, Sharon Shoham
13. Coq Coq correct! verification of type checking and erasure for Coq, in Coq · Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, Théo Winterhalter
14. Decidable subtyping for path dependent types · Julian Mackay, Alex Potanin, Jonathan Aldrich, Lindsay Groves
15. Deciding memory safety for single-pass heap-manipulating programs · Umang Mathur, Adithya Murali, Paul Krogmeier, P. Madhusudan, Mahesh Viswanathan
16. Decomposition diversity with symmetric data and codata · David Binder, Julian Jabs, Ingo Skupin, Klaus Ostermann
17. Deductive verification with ghost monitors · Martin Clochard, Claude Marché, Andrei Paskevich
18. Dependent type systems as macros · Stephen Chang, Michael Ballantyne, Milo Turner, William J. Bowman
19. Detecting floating-point errors via atomic conditions · Daming Zou, Muhan Zeng, Yingfei Xiong, Zhoulai Fu, Lu Zhang, Zhendong Su
20. Deterministic parallel fixpoint computation · Sung Kook Kim, Arnaud J. Venet, Aditya V. Thakur
21. Disentanglement in nested-parallel programs · Sam Westrick, Rohan Yadav, Matthew Fluet, Umut A. Acar
22. Does blame shifting work? · Lukas Lazarek, Alexis King, Samanvitha Sundar, Robert Bruce Findler, Christos Dimoulas
23. Executable formal semantics for the POSIX shell · Michael Greenberg, Austin J. Blatt
24. Fast, sound, and effectively complete dynamic race prediction · Andreas Pavlogiannis
25. Formal verification of a constant-time preserving C compiler · Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie + 1 more
26. Full abstraction for the quantum lambda-calculus · Pierre Clairambault, Marc de Visme
27. Graduality and parametricity: together again for the first time · Max S. New, Dustin Jamner, Amal Ahmed
28. Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time · Steffen Smolka, Nate Foster, Justin Hsu, Tobias Kappé, Dexter Kozen, Alexandra Silva
29. Incorrectness logic · Peter W. O'Hearn
30. Interaction trees: representing recursive and impure programs in Coq · Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce + 1 more
31. Kind inference for datatypes · Ningning Xie, Richard A. Eisenberg, Bruno C. d. S. Oliveira
32. Label-dependent session types · Peter Thiemann, Vasco T. Vasconcelos
33. Liquidate your assets: reasoning about resource usage in liquid Haskell · Martin A. T. Handley, Niki Vazou, Graham Hutton
34. Mechanized semantics and verified compilation for a dataflow synchronous language with reset · Timothy Bourke, Lélio Brun, Marc Pouzet
35. Optimal approximate sampling from discrete probability distributions · Feras A. Saad, Cameron E. Freer, Martin C. Rinard, Vikash K. Mansinghka
36. Par means parallel: multiplicative linear logic proofs as concurrent functional programs · Federico Aschieri, Francesco A. Genco
37. Parameterized verification under TSO is PSPACE-complete · Parosh Aziz Abdulla, Mohamed Faouzi Atig, Rojin Rezvan
38. Partial type constructors: or, making ad hoc datatypes less ad hoc · Mark P. Jones, J. Garrett Morris, Richard A. Eisenberg
39. Persistency semantics of the Intel-x86 architecture · Azalea Raad, John Wickerson, Gil Neiger, Viktor Vafeiadis
40. Pointer life cycle types for lock-free data structures with memory reclamation · Roland Meyer, Sebastian Wolff
41. Program synthesis by type-guided abstraction refinement · Zheng Guo, Michael James, David Justo, Jiaxiao Zhou, Ziteng Wang, Ranjit Jhala + 1 more
42. Provenance-guided synthesis of Datalog programs · Mukund Raghothaman, Jonathan Mendelson, David Zhao, Mayur Naik, Bernhard Scholz
43. Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time · Peixin Wang, Hongfei Fu, Krishnendu Chatterjee, Yuxin Deng, Ming Xu
44. PλωNK: functional probabilistic NetKAT · Alexander Vandenbroucke, Tom Schrijvers
45. Recurrence extraction for functional programs through call-by-push-value · G. A. Kavvos, Edward Morehouse, Daniel R. Licata, Norman Danner
46. Reduction monads and their signatures · Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi
47. Reductions for safety proofs · Azadeh Farzan, Anthony Vandikas
48. Relational proofs for quantum programs · Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, Li Zhou
49. RustBelt meets relaxed memory · Hoang-Hai Dang, Jacques-Henri Jourdan, Jan-Oliver Kaiser, Derek Dreyer
50. Semantics of higher-order probabilistic programs with conditioning · Fredrik Dahlqvist, Dexter Kozen
51. Seminaïve evaluation for a higher-order functional language · Michael Arntzenius, Neel Krishnaswami
52. Spy game: verifying a local generic solver in Iris · Paulo Emílio de Vilhena, François Pottier, Jacques-Henri Jourdan
53. Stacked borrows: an aliasing model for Rust · Ralf Jung, Hoang-Hai Dang, Jeehoon Kang, Derek Dreyer
54. SyTeCi: automating contextual equivalence for higher-order programs with references · Guilhem Jaber
55. Synthesis of coordination programs from linear temporal specifications · Suguman Bansal, Kedar S. Namjoshi, Yaniv Sa'ar
56. Synthesizing replacement classes · Malavika Samak, Deokhwan Kim, Martin C. Rinard
57. Taylor subsumes Scott, Berry, Kahn and Plotkin · Davide Barbarossa, Giulio Manzonetto
58. The fire triangle: how to mix substitution, dependent elimination, and effects · Pierre-Marie Pédrot, Nicolas Tabareau
59. The future is ours: prophecy variables in separation logic · Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer + 1 more
60. The high-level benefits of low-level sandboxing · Michael Sammler, Deepak Garg, Derek Dreyer, Tadeusz Litak
61. The next 700 relational program logics · Kenji Maillard, Catalin Hritcu, Exequiel Rivas, Antoine Van Muylder
62. The weak call-by-value λ-calculus is reasonable for both time and space · Yannick Forster, Fabian Kunze, Marc Roth
63. Towards verified stochastic variational inference for probabilistic programs · Wonyeol Lee, Hangyeol Yu, Xavier Rival, Hongseok Yang
64. Trace types and denotational semantics for sound programmable inference in probabilistic languages · Alexander K. Lew, Marco F. Cusumano-Towner, Benjamin Sherman, Michael Carbin, Vikash K. Mansinghka
65. Undecidability of d<: and its decidable fragments · Jason Z. S. Hu, Ondrej Lhoták
66. Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation · Mengqi Liu, Lionel Rieg, Zhong Shao, Ronghui Gu, David Costanzo, Jung-Eun Kim + 1 more
67. Visualization by example · Chenglong Wang, Yu Feng, Rastislav Bodík, Alvin Cheung, Isil Dillig
68. What is decidable about gradual types? · Zeina Migeed, Jens Palsberg