ESOP 2015
Tue 14 - Thu 16 April 2015 London, United Kingdom
Wed 15 Apr 2015 12:00 - 12:30 at Skeel - Session 4 Chair(s): Lars Birkedal

Datatypes and codatatypes are useful for specifying and reasoning about (possibly infinite) computational processes. The Isabelle/HOL proof as- sistant has recently been extended with a definitional package that supports both. We describe a complete procedure for deriving nonemptiness witnesses in the general mutually recursive, nested case—nonemptiness being a proviso for intro- ducing types in higher-order logic.

Wed 15 Apr
Times are displayed in time zone: Azores change

10:30 - 12:30: Session 4ESOP at Skeel
Chair(s): Lars BirkedalAarhus University
10:30 - 11:00
The Problem of Programming Language Concurrency Semantics
Mark BattyUniversity of Cambridge, Kayvan MemarianUniversity of Cambridge, Kyndylan NienhuisUniversity of Cambridge, Jean Pichon-PharabodUniversity of Cambridge, Peter SewellUniversity of Cambridge
11:00 - 11:30
The Best of Both Worlds: Trading Efficiency and Optimality in Fence Insertion for TSO
Parosh Aziz Abdulla, Mohamed Faouzi AtigUppsala University, Tuan Phong NgoUppsala University
11:30 - 12:00
Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity
Ilya SergeyIMDEA Software Institute, Aleksandar NanevskiIMDEA Software Institute, Anindya BanerjeeIMDEA Software Institute
12:00 - 12:30
Witnessing (Co)datatypes
Jasmin BlanchetteTU Munich, Andrei PopescuMiddlesex University, London, Dmitriy TraytelTU Munich