Home

Welcome

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.

Recently, in collaboration with CSIRO Data61 (formerly NICTA), I have been working on designing a linear-typed programming language to aid verification of file systems called Cogent. In the past I have worked on the l4.verified project and tools for the Isabelle theorem prover.

This contains my blog as well as a CV and other miscellany.

Posts

…or you can find more in the archives.

Tags

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 model-checking monads nicta paradox parallelism patch-theory plos publication quickcheck reasoning sapling semantics separation-logic slides standard-ml stm term-representation testing theorem-proving total type-theory types unsw verification version-control