Research output per year
Research output per year
Personal profile
Research Interests
My main research interests focus on the fruitful intersection of programming languages and formal methods. In particular, I am interested in type systems and type theories as ways to reduce cost of systems verification, the integration of automatic and manual verification techniques, and refinement frameworks and models that allow for both rich specifications and efficient implementations.
Qualifications
BSc (Hons.) Computer Science, University of New South Wales, 2012
PhD Computer Science, University of New South Wales, 2019
Biography
Liam O'Connor is a Lecturer in Programming Languages for Trustworthy Systems at the University of Edinburgh in the School of Informatics and part of the Laboratory for Foundations of Computer Science. He received his BSc Hons. degree in 2012 from the University of New South Wales in Sydney, Australia. From 2012 he worked at National ICT Australia (now data61, part of CSIRO) on formal verification of software systems including the formally verified microkernel seL4. This work eventually culminated in his doctorate, which he received in 2019. For his doctorate he designed the functional systems programming language Cogent, which includes a verification framework based around certifying compilation. Liam has also published in the area of dependently-typed programming and proving, and has other interests ranging from concurrency to software engineering.
Fingerprint
Dive into the research topics where Liam O'Connor is active. These topic labels come from the works of this person. Together they form a unique fingerprint.
- 12 Similar Profiles
Network
Recent external collaboration on country level. Dive into details by clicking on the dots or
Research output
-
Deferring the Details and Deriving Programs
O'Connor, L., 18 Aug 2019, Proceedings of the 4th ACM SIGPLAN International Workshop on Type-Driven Development. New York, NY, USA: ACM Association for Computing Machinery, p. 27–39 13 p.Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
-
Bringing Effortless Refinement of Data Layouts to Cogent
O'Connor, L., Chen, Z., Susarla, P., Rizkallah, C., Klein, G. & Keller, G., 29 Oct 2018, Leveraging Applications of Formal Methods, Verification and Validation. Modeling: 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part I. Margaria, T. & Steffen, B. (eds.). Cham: Springer International Publishing, p. 134-149 16 p. (Lecture Notes in Computer Science; vol. 11244).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
-
Provably trustworthy systems
Klein, G., Andronick, J., Keller, G., Matichuk, D., Murray, T. & O'Connor, L., 4 Sep 2017, In: Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences. 375, 2104, 23 p., 20150404.Research output: Contribution to journal › Article › peer-review
-
The COGENT Case for Property-Based Testing
Chen, Z., O'Connor, L., Keller, G., Klein, G. & Heiser, G., 31 Oct 2017, Proceedings of the 9th Workshop on Programming Languages and Operating Systems. New York, NY, USA: ACM Association for Computing Machinery, p. 1–7 7 p.Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
-
A Framework for the Automatic Formal Verification of Refinement from Cogent to C
Rizkallah, C., Lim, J., Nagashima, Y., Sewell, T., Chen, Z., O'Connor, L., Murray, T., Keller, G. & Klein, G., 7 Aug 2016, Interactive Theorem Proving: 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings. Blanchette, J. C. & Merz, S. (eds.). Cham: Springer International Publishing, p. 323-340 18 p. (Lecture Notes in Computer Science; vol. 9807).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution