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 an extension of Kobayashi's type-based approach to liveness properties, see THORS. For a decidability result about HORS plus a case construct see HORSC.

Game semantics

We investigate how to decide observational equivalence of fragments of Reynolds' Idealized Algol using game semantics.

• Call-by-name: HOMER Web interface, HOMER publication
• Call-by-value: HECTOR Web interface, Decidability result

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.