ESOP 2016 programme

• Nate Foster, Dexter Kozen, Konstantinos Mamouras, Mark Reitblatt and Alexandra Silva. Probabilistic NetKAT
• Andreas Lochbihler. Probabilistic functions and cryptographic oracles in higher order logic
• Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja and Federico Olmedo. Weakest precondition reasoning for expected run-times of probabilistic programs (EATCS award nominee)
• Daniel Huang and Greg Morrisett. An application of computable distributions to the semantics of probabilistic programming languages (EAPLS award nominee)

• Steven Keuchel, Stephanie Weirich and Tom Schrijvers. Needle & knot: binder boilerplate tied up
• Richard A. Eisenberg, Stephanie Weirich and Hamidhasan Ahmed. Visible type application
• Alejandro Serrano and Jurriaan Hage. Type error diagnosis for embedded DSLs by two-stage specialized type rules
• Ambrose Bonnaire-Sergeant, Sam Tobin-Hochstadt and Rowan Davies. Practical optional types for Clojure

Room: Blauwe Zaal (Chair: Peter Thiemann)
ESOP Invited Talk: Cristina Lopes (University of California at Irvine, USA)

Simulating Cities: A Software Engineering Perspective

Abstract: Despite all the reasons why complex simulations are desirable for decision and policy making, and despite advances in computing power, large distributed simulations of urban areas are still rarely used, with most of their adoption in military applications. The reality is that developing distributed simulations is much harder than developing non-distributed, specialized ones, and requires a much higher level of software engineering expertise.
This talk looks at urban simulations from a software engineering and systems design perspective, and puts forward the idea that non-traditional decompositions in simulation load management are not just beneficial for these applications, but are likely the only way to move that field forward.

• Tony Garnock-Jones and Matthias Felleisen. Coordinated concurrent programming in Syndicate
• Christopher Schuster, Tim Disney and Cormac Flanagan. Macrofication: refactoring by reverse macro expansion
• Yuting Wang and Gopalan Nadathur. The higher-order abstract syntax approach to verified transformations on functional programs
• Hideyuki Kawabata and Hideya Iwasaki. Improving floating-point numbers: a lazy approach to adaptive accuracy refinement for numerical computations
• Nicolas Feltman, Kayvon Fatahalian, Umut Acar and Carlo Angiuli. Automatically splitting a two-stage lambda calculus

• Dimitrios Kouzapas, Jorge A. Pérez and Nobuko Yoshida. On the relative expressiveness of higher-order session processes
• Emile Bres, Rob Van Glabbeek and Peter Höfner. T-AWN: a timed process algebra for wireless networks
• Emanuele D'Osualdo and C.-H. Luke Ong. On hierarchical communication topologies in the pi-calculus
• Johannes Åman Pohjola and Joachim Parrow. The expressive power of monotonic parallel composition

• Scott Owens, Magnus O. Myreen, Ramana Kumar and Yong Kiam Tan. Functional big-step semantics
• Gregory Malecha and Jesper Bengtson. Easy and efficient automation through reflective tactics
• Cláudio Belo Lourenço, Maria João Frade and Jorge Sousa Pinto. Formalizing single-assignment program verification: an adaptation-complete approach
• Alexander J. Summers and Peter Müller. Actor services: modular verification of message passing programs

• Pierre-Marie Pédrot and Alexis Saurin. Classical by-need
• Thomas Ehrhard. A functional language extending call-by-name and call-by-value, and its connection with linear logic
• Rodolphe Lepigre. A realizability model for a semantical value restriction
• Kasper Svendsen, Filip Sieczkowski and Lars Birkedal. Transfinite step-indexing: decoupling concrete and logical steps

• Jacques Carette and Amr Sabry. Computing with semirings and weak rig groupoids
• Antoine Miné, Jason Breck and Thomas Reps. An algorithm inspired by constraint solvers to infer inductive invariants in numeric programs (EASST award nominee)
• Rajeev Alur, Dana Fisman and Mukund Raghothaman. Regular programming for quantitative properties of data streams
• Pedro Da Rocha Pinto, Thomas Dinsdale-Young, Philippa Gardner and Julian Sutherland. Modular termination verification for non-blocking concurrency