avatar

Litao Zhou

周李韬
Ph.D. Candidate
University of Hong Kong
ltzhou (at) cs.hku.hk


About Me

I am a Ph.D. candidate in Computer Science at The University of Hong Kong, advised by Prof. Bruno C. d. S. Oliveira. My work spans type systems, including recursive types, subtyping, and modular programming (POPL’23 / JFP’25 / OOPSLA’24 / POPL’25), as well as foundational program verification with separation logic (VST-A, POPL’24). Ongoing work includes foundations to recursive modules in ML-family languages.

Before HKU, I received my B.Eng. from the IEEE Pilot Class at Shanghai Jiao Tong University, where I worked with Prof. Qinxiang Cao on foundationally sound verification of C programs (VST-A). Most recently, I was a Research Engineer at Inria Paris (Team Cambium), working with Didier Rémy.

I expect to graduate in August 2027 and am on the academic job market. See my Curriculum Vitae.

News

Publications

  1. Recursive Subtyping for All
    Litao Zhou*, Yaoda Zhou*, Qianyong Wan, Bruno C. d. S. Oliveira (*equal contribution)
    Journal of Functional Programming (JFP), 2025.
    PDF DOI Artifact Slides (Lyon & Paris) Extended version of POPL'23 paper

  2. QuickSub: Efficient Iso-Recursive Subtyping
    Litao Zhou, Bruno C. d. S. Oliveira
    52nd ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2025.
    PDF DOI Artifact Slides (Canberra) Slides (Denver) Appendix

  3. Full Iso-Recursive Types
    Litao Zhou, Qianyong Wan, Bruno C. d. S. Oliveira
    Object-oriented Programming, Systems, Languages, and Applications (OOPSLA), 2024.
    PDF DOI Artifact Slides

  4. VST-A: A Foundationally Sound Annotation Verifier
    Litao Zhou, Jianxing Qin, Qinshi Wang, Andrew W. Appel, Qinxiang Cao
    51st ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2024.
    PDF DOI Artifact

  5. Recursive Subtyping for All
    Litao Zhou*, Yaoda Zhou*, Bruno C. d. S. Oliveira (*equal contribution)
    50th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2023.
    PDF DOI Artifact Selected for Special Issue of Journal of Functional Programming

Extended Abstracts

  1. Compositional Programming with Full Iso-recursive Types
    Litao Zhou
    Student Research Competition, 51st ACM SIGPLAN Symposium on Principles of Programming Languages (POPL SRC), 2024.
    Abstract Poster Demo

  2. Foundationally Sound Annotation Verifier via Control Flow Splitting
    Litao Zhou
    Student Research Competition, ACM SIGPLAN conference on Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH SRC), 2022.
    Abstract Poster Slides 3rd Prize, Graduate Category

Education & Awards

Talks

Service


Powered by Jekyll and Minimal Light theme.