Dr. Liam O’Connor
4th October 2020


I am Liam O’Connor, a 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 am involved in supervisory duties for Informatics 1A on Functional Programming.

I work regularly in and on the Haskell programming language and the Agda proof assistant. Much of my research work involves these languages.

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

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