Publications
liamoc.net

Quickstrom and LTL Testing

A project with Oskar Wickström bringing the power of property-based testing to web application interface testing. More information is available at the Quickstrom website. This section also includes broader theoretical investigations into testing for linear temporal logics and related topics.

Liam O'Connor, Oskar Wickström
Quickstrom: Property-based Acceptance Testing with LTL Specifications
Programming Languages Design and Implementation (PLDI), pp. 1025-1038, San Diego, California, USA, June 2022.
Available from arXiv Talk available on YouTube

Rayhana Amjad, Rob van Glabbeek, Liam O'Connor
Semantics for Linear-time Temporal Logic with Finite Observations Expressiveness in Concurrency and Structural Operational Semantics (EXPRESS/SOS), pp. 35-50, Calgary, Canada, September 2024
Available from ETPCS Proofs on AFP

Cogent

A project at the Trustworthy Systems Group aimed at using programming languages with interesting types to aid verification of low-level systems. More information is available at the Cogent website.

Zilin Chen, Ambroise Lafont, Liam O'Connor, Gabriele Keller, Craig McLaughlin, Vincent Jackson, Christine Rizkallah
Dargent: A Silver Bullet for Verified Data Layout Refinement
Principles of Programming Languages (POPL), Boston, Massachusetts, USA, 2023.
Proceedings of the ACM on Programming Languages, Volume 7, January 2023, Article 47, pp 1369–1395
Available from TS Talk available on YouTube

Zilin Chen, Christine Rizkallah, Liam O'Connor, Partha Susarla, Gerwin Klein, Gernot Heiser, Gabriele Keller
Property-Based Testing: Climbing the Stairway to Verification
Software Language Engineering (SLE), pp. 84-97, Auckland, New Zealand, December 2022.
Winner of Distinguished Artifact Award.
Available from TS

Louis Cheung, Liam O'Connor, Christine Rizkallah
Overcoming Restraint: Composing Verification of Foreign Functions with Cogent
Certified Programs and Proofs (CPP), pp. 13-26, Philadelphia, Pennsylvania, USA, January 2022.
Available from arXiv Talk available on YouTube

Liam O'Connor, Zilin Chen, Christine Rizkallah, Vincent Jackson, Sidney Amani, Gerwin Klein, Toby Murray, Thomas Sewell, Gabriele Keller
Cogent: Uniqueness types and Certifying Compilation
Journal of Functional Programming, Volume 31, Issue on Secure Compilation, October 2021.
Available from CUP

Liam O'Connor
Type Systems for Systems Types
PhD Thesis, Computer Science and Engineering, Faculty of Engineering, University of New South Wales, 2019
Available from UNSWorks

Liam O'Connor, Zilin Chen, Partha Susarla, Christine Rizkallah, Gerwin Klein, Gabriele Keller
Bringing effortless refinement of data layouts to Cogent
International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA), LNCS v. 11244, pp. 134-149, Limassol, Cyprus, November, 2018
Available from TS

Gerwin Klein, June Andronick, Gabriele Keller, Daniel Matichuk, Toby Murray, Liam O'Connor
Provably Trustworthy Systems
Philosophical Transactions of the Royal Society A, Volume 375, Issue 2104.
Available from the Royal Society

Zilin Chen, Liam O'Connor, Gabriele Keller, Gerwin Klein and Gernot Heiser
The Cogent Case for Property-Based Testing
Workshop on Programming Languages and Operating Systems (PLOS), pp. 1-7, Shanghai, China, October, 2017
Available from TS

Liam O'Connor, Zilin Chen, Christine Rizkallah, Sidney Amani, Japheth Lim, Toby Murray, Yutaka Nagashima, Thomas Sewell, Gerwin Klein
Refinement through Restraint: Bringing Down the Cost of Verification
International Conference on Functional Programming (ICFP), pp. 89-102, Nara, Japan, September 2016.
Available from TS Talk available on YouTube

Christine Rizkallah, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Zilin Chen, Liam O'Connor, Toby Murray, Gabriele Keller and Gerwin Klein
A Framework for the Automatic Formal Verification of Refinement From Cogent to C
International Conference on Interactive Theorem Proving (ITP), LNCS v. 9087, pp. 323-340, Nancy, France, August 2016.
Available from TS

Sidney Amani, Alex Hixon, Zilin Chen, Christine Rizkallah, Peter Chubb, Liam O'Connor, Joel Beeren, Yutaka Nagashima, Japheth Lim, Thomas Sewell, Joseph Tuong, Gabriele Keller, Toby Murray, Gerwin Klein and Gernot Heiser
Cogent: Verifying High-assurance File System Implementations
International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pp. 175-188, Atlanta, GA, USA, April 2016.
Available from TS

Liam O'Connor, Gabriele Keller, Sidney Amani, Toby Murray, Gerwin Klein, Zilin Chen and Christine Rizkallah
CDSL Version 1: Simplifying Verification with Linear Types
Technical Report, NICTA, October, 2014.
Available from TS

Gabriele Keller, Toby Murray, Sidney Amani, Liam O'Connor, Zilin Chen, Leonid Ryzhyk, Gerwin Klein and Gernot Heiser
File Systems Deserve Verification Too!
Workshop on Programming Languages and Operating Systems (PLOS), pp. 1-7, Farmington, Pennsylvania, USA, November, 2013
A revised version of this paper was published in Operating Systems Review, Volume 48, Issue 1, January 2014, pages 58-64.
Available from TS

Dependent types and type systems

Liam O'Connor
Deferring the Details and Deriving Programs
Workshop on Type-Driven Development (TyDe), pp. 27-39, Berlin, Germany, August, 2019.
Available here Talk available on YouTube

Liam O'Connor
Applications of Applicative Proof Search
Workshop on Type-Driven Development (TyDe), pp. 43-55, Nara, Japan, September, 2016.
Available here Talk available on YouTube

Liam O'Connor
Formalising GHC's Type System
Undergraduate Thesis, UNSW, 2012.
Available here

Miscellaneous

Xueying Qin, Liam O'Connor, Rob van Glabbeek, Peter Höfner, Ohad Kammar and Michel Steuwer
Shoggoth: A Formal Foundation for Strategic Rewriting
Principles of Programming Languages (POPL), London, UK, 2024.
Proceedings of the ACM on Programming Languages, Volume 8, January 2024, Article 3, pp 61–89
Available from ACM

Xueying Qin, Liam O'Connor and Michel Steuwer
Primrose: Selecting Container Data Types by Their Properties
The Art, Science, and Engineering of Programming, Vol. 7, Issue 3, Article 11, 2023
Available from ‹Programming›

Liam O'Connor and Rayhana Amjad
Holbert: Reading, Writing, Proving and Learning in the Browser
Human Aspects of Types and Reasoning Assistants (HATRA), Auckland, New Zealand, 2022.
Live Version Here Available on arXiv Talk available on YouTube

Yutaka Nagashima and Liam O'Connor
Close Encounters of the Higher Kind: Emulating Constructor Classes in Standard ML
Workshop on ML 2016, Nara, Japan, September, 2016.
Available from TS Talk available on YouTube

Liam O'Connor
Gentzen: A Beginner's Proof Assistant based on Higher Order Logic
Undergraduate Project, UNSW, 2012
Available here