Litao Zhou (Tony)

Litao Zhou (Tony)

Junior Bachelor Student

Shanghai Jiao Tong University


Hi, this is Tony, a junior Computer Science student in Shanghai Jiao Tong University.

Coding is fun / What’s past is prologue

My research interest includes Programming Language, Functional Programming and Formal Verification. I am actively looking for a PL PhD position in 2022 fall.

Download my resumé.

  • Formal Verification
  • Programming Languages
  • Functional Programming
  • Non-Graduating Exchange Student, 2021 Fall

    National University of Singapore (School of Computing)

  • BSc in Computer Science (IEEE Pilot Class), 2018-2022(Expected)

    Shanghai Jiao Tong University


Software Engineer Intern
Sep 2020 – Jan 2021 Shanghai
In Visual and Parallel Computing Group, developed a web-based automation tool to smooth the testing workflow of graphics drivers.
Research Intern
Jul 2020 – Present Shanghai Jiao Tong University, Shanghai

Participate in following projects in Programming Languages.

  • Used OCaml to implement some instances of interpreters, compilers and virtual machine models of lambda calculus.
  • Using Teyjus, a high-order logic programming language, to implement various functional language compilation phases (e.g., lambda lifting, uncurrying, lambda shrinking).
  • Prove the correctness(semantic preservation) of the above compilation transformations using logical relations in Abella (Still ongoing)
Research Intern
Jan 2019 – Present Shanghai Jiao Tong University, Shanghai

Participate in following projects in Formal Verification using Coq.

  • Verify the correctness of the theory of real number construction.
  • Reason about the functional correctness of several classical graph algorithms (e.g., Tarjan’s algorithm for Strongly-Connected-Components) and their C implementations in VST.
  • Build and prove the soundness of a control-flow splitting tool based on VST to simplify verification proof of assertion-annotated C programs.