Monday, 19 Sep 2016

09:25am - 09:30am

Registration

09:30am - 10:30am

Automata-based analysis of threaded programs (PDF)
Markus Mueller-Olm, Universität Münster, Germany

10:30am - 11:00am

--- Group Photo & Coffee Break ---

11:00am - 12:00nn

Systems with parametric thread creation (PDF)
Igor Walukiewicz, Université Bordeaux and Centre National de la Recherche Scientifique, France

12:00nn - 02:30pm

--- Lunch Break ---

02:30pm - 03:30pm

Nested words for order-2 pushdown systems (PDF)
Aiswarya Cyriac, Chennai Mathematical Institute, India

03:30pm - 04:00pm

--- Coffee Break ---

04:00pm - 05:00pm

Summaries for context-free games (PDF)
Roland Meyer, University of Kaiserslautern, Germany

Tuesday, 20 Sep 2016

09:25am - 09:30am

Registration

09:30am - 12:00nn

Tutorial: Verification of concurrent data structures (PDF)
Ahmed Bouajjani, University Paris Diderot, Paris 7, France

12:00nn - 02:00pm

--- Lunch Break ---

02:00pm - 03:30pm

Tutorial: Introduction to collapsible pushdown automata and higher-order recursion schemes (PDF)
Pawel Parys, University of Warsaw, Poland

03:30pm - 04:00pm

--- Coffee Break ---

04:00pm - 05:30pm

Tutorial: Applications of higher-order model checking to program verification (PDF)

Hiroshi Unno, University of Tsukuba, Japan

Wednesday, 21 Sep 2016

09:25am - 09:30am

Registration

09:30am - 10:15am

Higher-order model checking in direct style (PDF)
Taku Terao, The University of Tokyo, Japan

10:15am - 11:00am

Nominal games: a semantics paradigm for effectful languages (PDF)
Nikos Tzevelekos, Queen Mary University of London, UK

11:00am - 11:30am

--- Coffee Break ---

11:30am - 12:15pm

Refinement types and higher-order constrained horn clauses (PDF)
Steven Ramsay, University of Oxford, UK

12:15pm - 01:00pm

Higher-order Buchi types (PDF)
Martin Hofmann, Ludwig-Maximilians-Universität München, Germany

01:00pm - 02:00pm

--- Lunch Break ---

Social Activities - Marina Bay

Thursday, 22 Sep 2016

09:25am - 09:30am

Registration

09:30am - 10:15am

How to decide quantitative properties for higher-order program with nature? (PDF)
Olivier Serre, Centre National de la Recherche Scientifique, France

10:15am - 10:45am

--- Coffee Break ---

10:45am - 11:30am

First steps towards probabilistic higher-order model-checking (PDF)
Charles Grellois, University Paris 7, France

11:30am - 12:15pm

On two notions of higher-order model checking (PDF)
Naoki Kobayashi, The University of Tokyo, Japan

12:15pm - 02:00pm

--- Lunch Break ---

02:00pm - 02:45pm

Modular verification of higher-order functional programs
Ryosuke Sato, University of Tokyo, Japan

02:45pm - 03:30pm

Finitary proof systems for Kozen's mu (PDF)
Bahareh Afshari, Technische Universität Wien, Austria

Graham Leigh, University of Gothenburg, Sweden

03:30pm - 04:00pm

--- Coffee Break ---

04:00pm - 04:45pm

Automata, logic and games for higher-type Bohm trees (PDF)
Luke Ong, University of Oxford, UK

04:45pm - 05:30pm

Negations in refinement intersection type systems (PDF)
Takeshi Tsukada, University of Tokyo, Japan

Friday, 23 Sep 2016

09:25am - 09:30am

Registration

09:30am - 10:15am

Compiling untyped Lambda Calculus to lower-level code by game semantics and partial evaluation (PDF)
Neil Jones, University of Copenhagen, Denmark

10:15am - 10:45am

--- Coffee Break ---

10:45am - 11:30am

Automata theory and game semantics of higher-order computation (PDF)
Andrzej Murawski, University of Warwick, UK