Welcome

I am Liam O’Connor, a Senior Lecturer¹ at the Australian National University School of Computing. I specialise in programming languages and type systems, verification, formal methods, and concurrency. I am also an Honorary Fellow in Programming Languages for Trustworthy Systems at the Laboratory for Foundations of Computer Science at the University of Edinburgh School of Informatics.

I do not yet have any teaching commitments at ANU. At Edinburgh, I tought courses on theoretical computer science, discrete mathematics, and concurrency theory.

I work regularly in and on the Haskell programming language and the Agda proof assistant. Much of my research work involves these languages. I am the Social Media Editor of the Journal of Functional Programming, and a Member-at-Large of the Steering Committee of TyDe.

I am the designer of the Holbert educational proof assistant.

I am also the lead researcher for the Quickstrom testing tool. This project is joint work with Oskar Wickström and my PhD student Rayhana Amjad (with Rob van Glabbeek as secondary supervisor).

I am also co-supervising a PhD student, Tudor Ferariu, on verification of blockchain smart contracts with Phil Wadler. I am also second supervisor to Mathieu Fehr, whose primary supervisor is Tobias Grosser.

Originally part of my doctorate and now as ongoing research work, I designed the Cogent programming language, and I remain a contributor to its associated verification framework and compiler. This project is part of the long-term vision of the Trustworthy Systems team (formerly at CSIRO Data61), to reduce the cost and effort required to make formally verified systems. In the past I have also worked with the Trustworthy Systems team on the l4.verified project and tools for the Isabelle theorem prover. I have also been affiliated with the DPH and Accelerate projects as my PhD supervisor was Gabriele Keller.

In my free time, I like to collect and tinker on old and obsolete computers. Please get in touch with me if you want to collaborate on retro computing projects, donate a computer, or visit to see my collection of old computers.

I am also an experienced liturgical singer and have extensively studied early church music from the middle ages.

This contains my blog as well as a publication list, and other miscellany.

Posts

• New position at ANU - 11th November 2024
• LTL semantics at EXPRESS/SOS - 10th Nov 2024
• Dargent (and Cogent) at POPL - 24th June 2023

…or you can find more in the archives.

Tags

abstraction agda anu aplas asplos blog category-theory cogent comp2111 competition compilers concurrency conference coq courses cpp dargent data-description data61 edsls express-sos ffi file-systems foundations fp-syd functional haskell hatra holbert icfp imperative isola itp jfp latex linear-types ltl ml-modules ml-workshop model-checking monads non-determinism paradox patch-theory pbt pldi plos popl publication quickcheck quickstrom reasoning refinement sapling semantics separation-logic sle slides splash standard-ml term-representation testing theorem-proving total tyde type-theory types unsw uoe verification version-control