Dr. Zilin Chen

Email
zilin <dot> chen <at> unswalumni <dot> com

A pdf version of my full CV can be obtained here.

Research Interests

My main research interests are in functional programming languages and their semantics, embedded domain-specific languages, program synthesise, type theories and software verification (in particular interactive theorem proving). I am also interested in logics, metamathematics, proof theories and other forms of formal methods. My research has a strong focus on applying formal methods to low-level systems programming.

Ghost Autonomy

Ghost was a start-up company founded in 2017, whose mission was to make self-driving for everyone. I joined their Sydney office in late 2022, freshly out from my PhD. I was hired to work on their custom deep learning model language, which was later replaced by PyTorch. I subsequently moved to work on deep learning models for vision-based perception for autonomous driving. The company ceased operation in Apr 2024.

Trustworthy Systems and Cogent

I was a member of the Trustworthy Systems group from 2013 to 2023. My main activities were around the Cogent project.
See project homepage for an overview, publications, people and other information.
The project is in dormant, but I am still maintaining the project in my spare time. [Github repo]

Education

PhD in Computer Science and Engineering, 2015 – 2023 (on program leave between 2019 – 2021)

Bachelor of Science (Honours Class 1), Computer Science, UNSW, 2011 – 2013

Publications

[1]	Zilin Chen. Towards A Practical High-Assurance Systems Programming Language. PhD thesis, CSE, UNSW Sydney, UNSW Sydney, Australia, March 2023. [ bib \| DOI \| http ]
[2]	Zilin Chen, Ambroise Lafont, Liam O’Connor, Gabriele Keller, Craig McLaughlin, Vincent Jackson, and Christine Rizkallah. Dargent: A silver bullet for verified data layout refinement. Proc. ACM Program. Lang., 7(POPL), January 2023. [ bib \| DOI \| http ]
[3]	Zilin Chen, Christine Rizkallah, Liam O'Connor, Partha Susarla, Gerwin Klein, Gernot Heiser, and Gabriele Keller. Property-based testing: Climbing the stairway to verification. In ACM SIGPLAN International Conference on Software Language Engineering, SLE 2022, Auckland, New Zealand, December 2022. ACM. [ bib \| DOI ]
[4]	Zilin Chen. A hoare logic style refinement types formalisation. In Proceedings of the 7th ACM SIGPLAN International Workshop on Type-Driven Development, TyDe 2022, page 1–14, New York, NY, USA, 2022. Association for Computing Machinery. [ bib \| DOI \| http ]
[5]	Liam O'Connor, Zilin Chen, Christine Rizkallah, Vincent Jackson, Sidney Amani, Gerwin Klein, Toby Murray, Thomas Sewell, and Gabriele Keller. Cogent: uniqueness types and certifying compilation. Journal of Functional Programming, 31:e25, 2021. [ bib \| DOI ]
[6]	Zilin Chen, Matt Di Meglio, Liam O'Connor, Partha Susarla Ajay, Christine Rizkallah, and Gabriele Keller. A data layout description language for Cogent (extended abstract), 2019. at PriSC. [ bib ]
[7]	Liam O'Connor, Zilin Chen, Partha Susarla, Christine Rizkallah, Gerwin Klein, and Gabriele Keller. Bringing effortless refinement of data layouts to Cogent. In Leveraging Applications of Formal Methods, Verification and Validation. Modeling: 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part I, page 134–149, Berlin, Heidelberg, 2018. Springer-Verlag. [ bib \| DOI \| http ]
[8]	Zilin Chen, Liam O'Connor, Gabriele Keller, Gerwin Klein, and Gernot Heiser. The Cogent case for property-based testing. In Proceedings of the 9th Workshop on Programming Languages and Operating Systems, PLOS'17, page 1–7, New York, NY, USA, 2017. Association for Computing Machinery. [ bib \| DOI \| http ]
[9]	Zilin Chen. Cogent^⇑: Giving systems engineers a stepping stone (extended abstract). In The workshop on Type-Driven Development, TyDe'17, 2017. [ bib \| .pdf ]
[10]	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. In Jasmin Christian Blanchette and Stephan Merz, editors, Interactive Theorem Proving, pages 323--340, Cham, 2016. Springer International Publishing. [ bib \| DOI \| http ]
[11]	Liam O'Connor, Zilin Chen, Christine Rizkallah, Sidney Amani, Japheth Lim, Toby Murray, Yutaka Nagashima, Thomas Sewell, and Gerwin Klein. Refinement through restraint: Bringing down the cost of verification. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, page 89–102, New York, NY, USA, 2016. Association for Computing Machinery. [ bib \| DOI \| http ]
[12]	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. In Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS '16, page 175–188, New York, NY, USA, 2016. Association for Computing Machinery. [ bib \| DOI \| http ]
[13]	Liam O'Connor, Gabriele Keller, Sidney Amani, Toby Murray, Gerwin Klein, Zilin Chen, and Christine Rizkallah. CDSL version 1: Simplifying verification with linear types, 2014-10. [ bib ]
[14]	Gabriele Keller, Toby Murray, Sidney Amani, Liam O'Connor, Zilin Chen, Leonid Ryzhyk, Gerwin Klein, and Gernot Heiser. File systems deserve verification too! In Proceedings of the Seventh Workshop on Programming Languages and Operating Systems, PLOS '13, New York, NY, USA, 2013. Association for Computing Machinery. [ bib \| DOI \| http ]