[4-22]Verification of Higher-Order Computation
Date:2008-04-17
Title：Verification of Higher-Order Computation
Speaker：Professor Luke Ong （Computing Laboratory, Oxford University, UK）
Time：3:00pm Tuesday April 22 2008
Venue：Lecture room of SKLCS
Abstract：
We survey recent developments in an approach to the verification of higher-order computation based on game semantics. 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 ranked trees and graphs. As applications of a representation theory of innocent strategies based on TRAVERSALS, we present a recent advance in the model checking of ranked trees generated by higher-order recursion schemes (we show that ranked trees generated by arbitrary higher-order recursion schemes have decidable monadic second-order theories), and the first machine characterization of recursion schemes (by a new variant class of higher-order pushdown automata called COLLAPSIBLE pushdown automata). We conclude with some speculative remarks about reachability checking of functional programs. A theme of the work is the fruitful interplay of ideas between the neighbouring fields of Semantics and Verification.
ct on that activity.
Bio：
Prof. Ong’s research has mainly been in Semantics of Computation, which is concerned with the development and analysis of mathematical structures that model computation using ideas and tools from Mathematical Logic. His thesis was about the Lazy Lambda Calculus as a foundation of functional programming. He has worked on Type Theory (semantics and generic strong normalization proofs), Linear Logic (game semantics, proof nets), computational proof theory (especially semantics, representation, and computational content of classical proofs), and semantics of programming languages (fully abstract game semantics of PCF). Recently his research has tended to be motivated by problems of an algorithmic nature. A focus is the use of (game-) semantic methods to study algorithmic properties of infinite structures generated by higher-order models of computation.