ESOP 2018

36 papers

1. A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification · Armaël Guéneau, Arthur Charguéraud, François Pottier
2. A Separation Logic for a Promising Semantics · Kasper Svendsen, Jean Pichon-Pharabod, Marko Doko, Ori Lahav, Viktor Vafeiadis
3. A Typing Discipline for Statically Verified Crash Failure Handling in Distributed Systems · Malte Viering, Tzu-Chun Chen, Patrick Eugster, Raymond Hu, Lukasz Ziarek
4. A Verified Compiler from Isabelle/HOL to CakeML · Lars Hupel, Tobias Nipkow
5. An Abstract Interpretation Framework for Input Data Usage · Caterina Urban, Peter Müller
6. An Assertion-Based Program Logic for Probabilistic Programs · Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
7. Behavioural Equivalence via Modalities for Algebraic Effects · Alex Simpson, Niels F. W. Voorneveld
8. Compositional Verification of Compiler Optimisations on Relaxed Memory · Mike Dodds, Mark Batty, Alexey Gotsman
9. Concurrent Kleene Algebra: Free Model and Completeness · Tobias Kappé, Paul Brunet, Alexandra Silva, Fabio Zanasi
10. Consistent Subtyping for All · Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira
11. Correctness of a Concurrent Object Collector for Actor Languages · Juliana Franco, Sylvan Clebsch, Sophia Drossopoulou, Jan Vitek, Tobias Wrigstad
12. Deadlock-Free Monitors · Jafar Hamin, Bart Jacobs
13. Deterministic Concurrency: A Clock-Synchronised Shared Memory Approach · Joaquín Aguado, Michael Mendler, Marc Pouzet, Partha S. Roop, Reinhard von Hanxleden
14. Dualizing Generalized Algebraic Data Types by Matrix Transposition · Klaus Ostermann, Julian Jabs
15. Evaluating Design Tradeoffs in Numeric Static Analysis for Java · Shiyi Wei, Piotr Mardziel, Andrew Ruef, Jeffrey S. Foster, Michael Hicks
16. Eventual Consistency for CRDTs · Radha Jagadeesan, James Riely
17. Explicit Effect Subtyping · Amr Hany Saleh, Georgios Karachalias, Matija Pretnar, Tom Schrijvers
18. Failure is Not an Option - An Exceptional Type Theory · Pierre-Marie Pédrot, Nicolas Tabareau
19. Fine-Grained Semantics for Probabilistic Programs · Benjamin Bichsel, Timon Gehr, Martin T. Vechev
20. Fragment Abstraction for Concurrent Shape Analysis · Parosh Aziz Abdulla, Bengt Jonsson, Cong Quy Trinh
21. HOBiT: Programming Lenses Without Using Lens Combinators · Kazutaka Matsuda, Meng Wang
22. Higher-Order Program Verification via HFL Model Checking · Naoki Kobayashi, Takeshi Tsukada, Keiichi Watanabe
23. How long, O Bayesian network, will I sample thee? - A program analysis perspective on expected sampling times · Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
24. Let Arguments Go First · Ningning Xie, Bruno C. d. S. Oliveira
25. Logical Reasoning for Disjoint Permissions · Xuan Bach Le, Aquinas Hobor
26. Modular Product Programs · Marco Eilers, Peter Müller, Samuel Hitz
27. On Parallel Snapshot Isolation and Release/Acquire Consistency · Azalea Raad, Ori Lahav, Viktor Vafeiadis
28. On Polymorphic Sessions and Functions - A Tale of Two (Fully Abstract) Encodings · Bernardo Toninho, Nobuko Yoshida
29. Paxos Consensus, Deconstructed and Abstracted · Álvaro García-Pérez, Alexey Gotsman, Yuri Meshman, Ilya Sergey
30. Program Verification by Coinduction · Brandon M. Moore, Lucas Peña, Grigore Rosu
31. Quantitative Analysis of Smart Contracts · Krishnendu Chatterjee, Amir Kafshdar Goharshady, Yaron Velner
32. Reasoning About a Machine with Local Capabilities - Provably Safe Stack and Return Pointer Management · Lau Skorstengaard, Dominique Devriese, Lars Birkedal
33. Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus · Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Ales Bizjak, Marco Gaboardi, Deepak Garg
34. Session-Typed Concurrent Contracts · Hannah Gommerstadt, Limin Jia, Frank Pfenning
35. Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq · Vincent Rahli, Ivana Vukotic, Marcus Völp, Paulo Jorge Esteves Veríssimo
36. Verified Learning Without Regret - From Algorithmic Game Theory to Distributed Systems with Mechanized Complexity Guarantees · Samuel Merten, Alexander Bagnall, Gordon Stewart