18th Estonian Winter School in Computer Science (EWSCS)
XVIII Eesti Arvutiteaduse Talvekool

Palmse, Estonia, March 3 - 8, 2013

Luke Ong

Dept. of Computer Science
University of Oxford
United Kingdom

Higher-Order Model Checking


This course is about the foundations and algorithms that underpin recent developments in the model checking of higher-order programs.

We begin by studying two models of higher-order computation: recursion schemes and collapsible pushdown automata.

Recursion schemes are in essence the simply-typed λ-calculus with recursion, generated from first-order symbols.

Collapsible pushdown automata are a generalisation of pushdown automata to higher-order stacks - which are iterations of stacks of stacks - that contain symbols equipped with links.

We study and compare the expressive power of the two models and the algorithmic properties of infinite structures such as trees and graphs generated by them.

We survey applications to the verification of higher-order functional programs, focussing on recent developments of "practical" algorithms.

A central theme is the fruitful interplay of ideas between the neighbouring fields of semantics and algorithmic verification.

Course materials

Valid CSS! Valid XHTML 1.0 Strict Last changed April 17, 2016 21:11 EET by local organizers, ewscs13(at)cs.ioc.ee
EWSCS'13 page: http://cs.ioc.ee/ewscs/2013/