ESOP 2017

36 papers

1. A Classical Sequent Calculus with Dependent Types · Étienne Miquey
2. A Higher-Order Logic for Concurrent Termination-Preserving Refinement · Joseph Tassarotti, Ralf Jung, Robert Harper
3. APLicative Programming with Naperian Functors · Jeremy Gibbons
4. Abstract Specifications for Concurrent Maps · Shale Xiong, Pedro da Rocha Pinto, Gian Ntzik, Philippa Gardner
5. Caper - Automatic Verification for Fine-Grained Concurrency · Thomas Dinsdale-Young, Pedro da Rocha Pinto, Kristoffer Just Andersen, Lars Birkedal
6. Commutative Semantics for Probabilistic Programming · Sam Staton
7. Comprehending Isabelle/HOL's Consistency · Ondrej Kuncar, Andrei Popescu
8. Conditional Dyck-CFL Reachability Analysis for Complete and Efficient Library Summarization · Hao Tang, Di Wang, Yingfei Xiong, Lingming Zhang, Xiaoyin Wang, Lu Zhang
9. Confluence of Graph Rewriting with Interfaces · Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski, Fabio Zanasi
10. Context-Free Session Type Inference · Luca Padovani
11. Contextual Equivalence for Probabilistic Programs with Continuous Random Variables and Scoring · Ryan Culpepper, Andrew Cobb
12. Disjoint Polymorphism · João Alpuim, Bruno C. d. S. Oliveira, Zhiyuan Shi
13. Extensible Datasort Refinements · Jana Dunfield
14. Faster Algorithms for Weighted Recursive State Machines · Krishnendu Chatterjee, Bernhard Kragl, Samarth Mishra, Andreas Pavlogiannis
15. Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants · Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel
16. Generalizing Inference Systems by Coaxioms · Davide Ancona, Francesco Dagnino, Elena Zucca
17. Incremental Update for Graph Rewriting · Pierre Boutillier, Thomas Ehrhard, Jean Krivine
18. Is Your Software on Dope? - Formal Analysis of Surreptitiously "enhanced" Programs · Pedro R. D'Argenio, Gilles Barthe, Sebastian Biewer, Bernd Finkbeiner, Holger Hermanns
19. LINCX: A Linear Logical Framework with First-Class Contexts · Aïna Linn Georges, Agata Murawska, Shawn Otis, Brigitte Pientka
20. Linearity, Control Effects, and Behavioral Types · Luís Caires, Jorge A. Pérez
21. ML and Extended Branching VASS · Conrad Cotton-Barratt, Andrzej S. Murawski, C.-H. Luke Ong
22. Metric Reasoning About \lambda -Terms: The General Case · Raphaëlle Crubillé, Ugo Dal Lago
23. Modular Verification of Higher-Order Functional Programs · Ryosuke Sato, Naoki Kobayashi
24. Modular Verification of Procedure Equivalence in the Presence of Memory Allocation · Tim Wood, Sophia Drossopoulou, Shuvendu K. Lahiri, Susan Eisenbach
25. Observed Communication Semantics for Classical Processes · Robert Atkey
26. Probabilistic Termination by Monadic Affine Sized Typing · Ugo Dal Lago, Charles Grellois
27. Programs Using Syntax with First-Class Binders · Francisco Ferreira, Brigitte Pientka
28. Proving Linearizability Using Partial Orders · Artem Khyzha, Mike Dodds, Alexey Gotsman, Matthew J. Parkinson
29. Tackling Real-Life Relaxed Concurrency with FSL++ · Marko Doko, Viktor Vafeiadis
30. Temporary Read-Only Permissions for Separation Logic · Arthur Charguéraud, François Pottier
31. The Essence of Functional Programming on Semantic Data · Martin Leinberger, Ralf Lämmel, Steffen Staab
32. The Essence of Higher-Order Concurrent Separation Logic · Robbert Krebbers, Ralf Jung, Ales Bizjak, Jacques-Henri Jourdan, Derek Dreyer, Lars Birkedal
33. The Power of Non-determinism in Higher-Order Implicit Complexity - Characterising Complexity Classes Using Non-deterministic Cons-Free Programming · Cynthia Kop, Jakob Grue Simonsen
34. Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic · Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger
35. Verified Characteristic Formulae for CakeML · Armaël Guéneau, Magnus O. Myreen, Ramana Kumar, Michael Norrish
36. Verifying Robustness of Event-Driven Asynchronous Programs Against Concurrency · Ahmed Bouajjani, Michael Emmi, Constantin Enea, Burcu Kulahcioglu Ozkan, Serdar Tasiran