Mjolnir

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.

Game semantics

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.

We developed Soter (Web interface), a tool that verifies coverability properties of (a substantial fragment of) Erlang. The algorithm uses Petri Net model checking as a back-end implemented by BFC.

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.