Luke Ong's Group
This is the homepage for Luke Ong's group, which carries out research in a number of different areas.
Verification of higher-order functional programs
Using decidability results about higher-order recursion schemes (HORS) and MSO, we look at the model-checking approach to verification of both call-by-name and call-by-value functional programming languages. For a decidability result about HORS plus a case construct see HORSC. For an extension of Kobayashi's type-based approach to liveness properties, see horsapt.
We investigate how to decide observational equivalence of fragments of Reynolds' Idealized Algol using game semantics.
Automated Analysis and Verification of Actor-style Concurrency
We investigate how to verify properties of extensions of functional languages with concurrency primitives inspired by the Actor Model with a combination of Static Analysis and Infinite-state Model Checking.
Information Security in Dynamically Typed Languages with Metaprogramming
We investigate how to verify information security properties in dynamically typed and untyped languages with metaprogramming facilities.
LOng Lunch seminar
We hold an informal seminar series for the presentation of new work within the group. Visitors and other members of the department are also welcome to give talks. We typically meet at 12:45 on Tuesdays in room 441 (051 and 380 are also sometimes used).
ICFP 2011 Programming Contest
(This is not strictly research.) Here is the readme from our winning entry to the ICFP 2011 Programming Contest. The contest task was to write a program to play a card game with a functional programing twist called Lambda: The Gathering. The readme gives a description of our strategy.
The team, Eta-LOng Normal Form, comprised four students from Luke Ong's group: Chris Broadbent, Martin Lester, Robin Neatherway and Steven Ramsay.