ESOP 2017 accepted papers

Étienne Miquey. A Classical Sequent Calculus with Dependent Types
Jeremy Gibbons. APLicative Programming with Naperian Functors
Davide Ancona, Francesco Dagnino and Elena Zucca.Generalizing inference systems by coaxioms
Francisco Ferreira and Brigitte Pientka. Programs Using Syntax with First-Class Binders
Krishnendu Chatterjee, Bernhard Kragl, Samarth Mishra and Andreas Pavlogiannis. Faster Algorithms for Weighted Recursive State Machines
Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu and Dmitriy Traytel. Friends with Benefits: Implementing Corecursion in Foundational Proof Assistants
Aina L. Georges, Agata Murawska, Shawn Otis and Brigitte Pientka. Lincx: A Linear Logical Framework with First-class Context
Ondřej Kunčar and Andrei Popescu.Comprehending Isabelle/HOL’s Consistency
Martin Leinberger, Ralf Lämmel and Steffen Staab. The essence of functional programming on semantic data
Hao Tang, Di Wang, Yingfei Xiong, Linngming Zhang, Xiaoyin Wang and Lu Zhang. Conditional Dyck-CFL Reachability Analysis for Complete and Efficient Library Summarization
Artem Khyzha, Mike Dodds, Alexey Gotsman and Matthew Parkinson. Proving Linearizability Using Partial Orders
Luis Caires and Jorge A. Pérez. Linearity, Control Effects, and Behavioural Types
Conrad Cotton-Barratt, Andrzej Murawski and Luke Ong. ML and Extended BVASS
Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski and Fabio Zanasi. Confluence of Graph Rewriting with Interfaces
Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll and Florian Zuleger. Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic
Gilles Barthe, Sebastian Biewer, Pedro R. D'Argenio, Bernd Finkbeiner and Holger Hermanns. Is your software on dope? -- Formal analysis of surreptitiously "enhanced" programs
Marko Doko and Viktor Vafeiadis. Tackling Real-Life Relaxed Concurrency with FSL++
Shale Xiong, Pedro Da Rocha Pinto, Gian Ntzik and Philippa Gardner. Abstract Specifications for Concurrent Maps
Arthur Charguéraud and François Pottier. Temporary Read-Only Permissions for Separation Logic
Pierre Boutillier, Thomas Ehrhard and Jean Krivine. Incremental update for graph rewriting
Robert Atkey. Observed Communication Semantics for Classical Processes
Robbert Krebbers, Ralf Jung, Aleš Bizjak, Jacques-Henri Jourdan, Derek Dreyer and Lars Birkedal. The Essence of Higher-Order Concurrent Separation Logic
Luca Padovani. Context-Free Session Type Inference
Cynthia Kop and Jakob Grue Simonsen. The Power of Non-Determinism in Higher-Order Implicit Complexity
Armaël Guéneau, Magnus O. Myreen, Ramana Kumar and Michael Norrish. Verified Characteristic Formulae for CakeML
Thomas Dinsdale-Young, Pedro Da Rocha Pinto, Kristoffer Just Andersen and Lars Birkedal. Caper: Automatic Verification for Fine-grained Concurrency
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Burcu Kulahcioglu Ozkan and Serdar Tasiran. Verifying Robustness of Event-Driven Asynchronous Programs against Concurrency
Ugo Dal Lago and Charles Grellois. Probabilistic Termination by Monadic Affine Sized Typing
Joshua Dunfield. Extensible Datasort Refinements
Joseph Tassarotti, Ralf Jung and Robert Harper. A Higher-Order Logic for Concurrent Termination-Preserving Refinement
Sam Staton.Commutative semantics for probabilistic programming
Tim Wood, Shuvendu K. Lahiri, Sophia Drossopoulou and Susan Eisenbach. Modular Verification of Procedure Equivalence in the Presence of Memory Allocation
Ryan Culpepper and Andrew Cobb. Contextual Equivalence for Probabilistic Programs with Continuous Random Variables and Scoring
João Alpuim, Bruno C. D. S. Oliveira and Zhiyuan Shi. Disjoint Polymorphism
Ryosuke Sato and Naoki Kobayashi. Modular Verification of Higher-order Functional Programs
Raphaëlle Crubillé and Ugo Dal Lago. Metric Reasoning about Lambda Terms: the General Case