CS SEMINAR

Higher-Order Constrained Horn Clauses and Refinement Types

Speaker
Prof Luke Ong
University of Oxford

Chaired by
Dr CHIN Wei Ngan, Associate Professor, School of Computing
chinwn@comp.nus.edu.sg

18 Aug 2017 Friday, 02:00 PM to 03:00 PM

Executive Classroom, COM2-04-02

Abstract:
Motivated by applications in automated verification of higher-order functional programs, we develop a notion of constrained Horn clauses in higher-order logic and a decision problem concerning their satisfiability.
We show that, although satisfiable systems of higher-order clauses do not generally have least models, there is a notion of canonical model obtained through a reduction to a problem concerning a kind of monotone logic program. Following work in higher-order program verification, we develop a refinement type system in order to reason about and automate the search for models. This provides a sound but incomplete method for solving the decision problem. Finally, we show that an extension of the decision problem in which refinement types are used directly as guards on existential quantifiers can be reduced to the original problem. This result can be used to show that properties of higher-order functions that are definable using refinement types are also expressible using higher-order constrained Horn clauses.
(This is joint work with Toby Cathcart Burn and Steven Ramsay.)
https://arxiv.org/abs/1705.06216

Biodata:
Luke Ong is Professor of Computer Science and Director of Graduate Studies, Department of Computer Science, University of Oxford; and Fellow of Merton College. He holds a BA in Mathematics (1984, Triple First) and a Postgraduate Diploma in Computer Science (1985, Distinction) from University of Cambridge, and PhD in Computer Science (1988) from Imperial College University of London. After a brief Lectureship at the National University of Singapore (1991) and a Prize Research Fellowship at Trinity College Cambridge (1992-1993), he was appointed to a University Lectureship at the University of Oxford in 1994, and promoted to Reader in 2002 and to Professor in 2004. He was a Visiting Professor at ??cole Normale Sup??rieure, Paris (1996), and the National University of Singapore (2004, 2014), Visiting Consultant at Bell Labs, Murray Hill, USA (2001), and Resident Member of the Isaac Newton Institute of Mathematical Sciences, Cambridge (1996, 2006).
Ong has worked in many areas in the semantics and logic of computation, including lambda calculus and types, concurrency, linear logic and computational proof theory. He has played a leading r??le in the development of game semantics. More recently his research has tended to be motivated by algorithmic problems. He has worked in software model checking, algorithmic game theory and computational economics, implicit computational complexity, and convergence and scalability in internet routing protocols. His current projects include higher-order model checking, actor concurrency, game semantics, algorithmic game theory, and language-based security.
Luke Ong is General Chair of ACM/IEEE Symposium on Logic in Computer Science (LICS), and Vice Chair of the ACM Special Interest Group in Logic and Computation (SIGLOG). He serves / has served on the council or steering committee of European Association of Theoretical Computer Science (EATCS), European Association of Computer Science Logic (EACSL), and European Joint Conferences on Theory and Practice of Software (ETAPS); he is a member of the steering committee of several conferences and workshops, including Foundations of Software Science and Computational Structures (FoSSaCS), Typed Lambda Calculus and Applications (TLCA), Games in Logic and Programming (GaLoP), and Logic and Computational Complexity (LCC). He was PC chair of CSL05, LICS07, IFIP TCS08, FoSSaCS10, TLCA11, TASE11 and WoLLIC12. He is a member of the Singapore Academic Research Council, and chairs their Informatics and Mathematics Expert Panel; he sits on the judging panel of the EACSL Ackermann Award and the EATCS Distinguished Dissertation Award. He has served on the editorial boards of the LMS Journal of Computation and Mathematics and Journal of Logical Methods in Computer Science. Ong has graduated 20, and currently (co)supervises 9, doctoral students at Oxford.