CORE PhD-Award for Liam O’Connor

Dr Liam O’Connor’s PhD Type Systems for Systems Types was awarded in October 2019, and it was this year (October 2020) the recipient of the Commendation (runner-up) CORE Award for the “Best PhD Thesis in our Field”. His topic spans Programming Languages, Formal Verification and Systems Programming.

The thesis title refers to the two conceptual components that O’Connor’s research brought together in such an original way. “Type Systems” are the tools available to programmers who want to state at compile-time the values their variables may take. Types can be as simple as “This variable must be an integer.” But in their modern form they can include attributes as complex as “This variable can be referenced to by at most one pointer, and must be properly disposed of.” The mathematical logic needed to check those latter types at compile time is formidable: the process is very complicated. But it is carried out by the compiler built by O’Connor; and as a result, the programmer can easily benefit from the types’ expressiveness, because the resulting programs will have fewer bugs and, often, more efficient implementations.

The other title phrase “Systems Types” refers to people, the operating-systems experts that deal with computers at the very lowest level. Generally, they are not formidable mathematical logicians. Instead, they are masters of the extremely complex and sometimes bizarre behaviours built in to modern processors, where modularity, elegance and even correctness (but accidentally) are sometimes sacrificed for performance: speed and power.

Dr O’Connor's thesis connected those two extremes in an astonishing way. He designed a high-level programming language Cogent, in the functional (i.e. mathematical) style. Its Type System includes  “uniqueness types” in a way that makes it possible to compile the program into two separate versions. The first version, in a mathematical/logical language, can be reasoned about reliably –by actual people– at a high level to see whether it does what it is supposed to do. And they can use mathematical tools to help with that reasoning, to check it, almost in a secondary-school algebraic style: “This program equals that program, and it in turn equals this other one…” The second version of the Cogent-compiled code is presented in the C programming language, a favourite of the Systems Types because it matches the hardware so closely (as it was originally designed to do); but algebraic reasoning does not work well in C.

Connecting those two far-apart versions is the job of Formal Verification: a proof that the high-level program and the C-code correspond, that they have the same behaviour, i.e. do the same thing. In that way, conclusions reached by people reasoning about the high-level program version can without further checking be expected to be realised by computers executing the C-code version.

Beyond producing two versions of the program however, Cogent generates as well the proof of their correspondence, automatically, and in a form that can be checked independently by a third party. Thus you can have your cake (do high-level program-algebraic reasoning about your program) and eat it too (run a C-language version of it on actual hardware). But you do not have to bake your cake: Cogent does that for you (the automatically generated proof of correspondence).

It is as described above that O’Connor's thesis has managed to balance three conflicting targets in a very sophisticated way: high-level reasoning, constrained by the intellectual capabilities of the program designers; low-level realities of computer hardware and the systems code that accesses it directly; and the adroit construction of long-distance connection between those two — lifting the high-level just as far as possible without losing the ability to generate automatically a machine-checkable proof that reaches, from there, all the way back to the low level again.

The CORE-Award Committee wrote that “The originality, scale and presentation of this research are outstanding. The panel considered the referees and examiners’ comments noting that the thesis is a ‘significant original contribution to computer science, in particular to the fields of programming languages and formal verification’.” One of the thesis examiners wrote that the thesis was “the best dissertation that he had ever read”. Both examiners recommended acceptance without modification.

UNSW’s School of Computer Science and Engineering has a long history –decades– of simultaneous excellence in these extremes, more generally in Operating Systems and in Formal Methods; and it has for many years managed to keep them in close physical proximity. An award like this is a wonderful outcome, one that that justly rewards and celebrates the synergy to which Dr O’Connor contributed and from which he benefited.