Dr. Liam O’Connor
4th October 2020


I am Liam O’Connor, a Lecturer in Programming Languages for Trustworthy Systems for LFCS at the University of Edinburgh School of Informatics. I specialise in programming languages and type systems, verification, formal methods, and concurrency.

In my previous posting at the University of New South Wales I taught several courses ranging from theory of programming languages to concurrency to formal methods. At Edinburgh, I am focusing primarily on research work for the moment, although I was involved in supervisory duties for Informatics 1A on Functional Programming, and in the coming semester I will be co-teaching Introduction to Theoretical Computer Science with Julian Bradfield.

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.

I am the designer of the Holbert educational proof assistant and co-ordinate undergraduate students on that project. Currently, my undergraduate students are Rayhana Amjad, Chris Perceval-Maxwell and Yining Liu.

I am also the lead researcher for the Quickstrom testing tool and have led efforts to design and implement a new specification language based on our QuickLTL variant of Linear Temporal Logic. This project is joint work with Oskar Wickström. I will be taking on a new PhD student on this topic in the near future, although the post is likely to be filled, I will update here if I need applicants.

I am also co-supervising a PhD student, Tudor Ferariu, on verification of blockchain smart contracts with Prof. Phil Wadler.

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 Prof. 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.

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


…or you can find more in the archives.


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