题目：Verification of Higher-Order Computation
报告人：Luke Ong 教授
　　　（Computing Laboratory, Oxford University, UK）
时间：2008年4月22日（星期二），下午3:00
地点：计算机科学国家重点实验室报告厅（5号楼三层）

摘要：
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.

报告人简介：
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.