I am Liam O'Connor, a computer science researcher, student and teacher, currently working at UNSW. I specialise in programming languages and type systems, verification, compilers, formal methods, concurrency and parallel programming.

As a member of the UNSW PLS Group, I work regularly in and on the Haskell programming language and the Agda proof assistant. I have strong interest in the PLS projects DPH, Accelerate and Disciple.

I am the designer of the Cogent language and a contributor to its associated verification framework and compiler. This project is part of the long-term vision of the Trustworthy Systems team at Data61, to reduce the cost and effort required to make formally verified systems. This project forms the basis of my PhD thesis. In the past I have also worked with the Trustworthy Systems team on the l4.verified project and tools for the Isabelle theorem prover.

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


…or you can find more in the archives.


agda aplas asplos blog category-theory cogent comp3151 competition compilers concurrency conference coq courses cpp data61 edsls file-systems foundations fp-syd functional hakyll haskell icfp imperative itp latex lecture linear-types ml-modules ml-workshop model-checking monads paradox parallelism patch-theory plos publication quickcheck reasoning sapling semantics separation-logic slides standard-ml stm term-representation testing theorem-proving total tyde type-theory types unsw verification version-control