Past Events in Computer Science

Departmental Seminar - Luke Ong (Oxford)

Title: An approach to the verification of higher-order infinite structures

Abstract: We survey recent developments in a systematic approach to the verification of higher-order computation. Higher-order recursion schemes are in essence (programs of) the simply-typed lambda calculus with recursion, generated from uninterpreted first-order symbols. They are a highly expressive definitional device for infinite structures such as word languages, infinite trees and graphs. As an algorithmic application of game semantics, we present recent advances in the model checking of infinite trees and graphs generated by recursion schemes, and a machine characterization of recursion schemes by a new variant class of higher-order pushdown automata called collapsible pushdown automata. We conclude with some applications to the verification of higher-order functional programs. A theme of the work is the fruitful interplay of ideas between the neighbouring fields of semantics and verification.

Short Bio: Luke Ong is Professor of Computer Science at the University of Oxford.
He was educated at Trinity College, Cambridge (BA Mathematics 1984, Diploma in Computer Science 1985) and Imperial College, London (PhD Computer Science 1988). His research has mainly been in semantics of computation. His current projects include algorithmic game semantics with applications to software model checking, and verification of infinite-state systems.

Contact shengchao.qin@durham.ac.uk for more information about this event.