Yiyuan Cao

PhD student in Programming Languages.

About me

I’m Yiyuan, a third-year PhD student in the Programming Languages Lab at the School of Computer Science, Peking University. My advisor is Prof. Zhenjiang Hu.

My research interest is in programming languages and program proofs in general. I maintain a list of learning resources for these topics as a Gist. I am particularly interested in how to develop verifiably safe, correct, and efficient programs in a productive manner, with the help of programming language techniques.

Education

2017 - 2022 Peking University, Beijing, China.

Bachelor of Science in Computer Science.

2022 - now Peking University, Beijing, China.

PhD student in Programming Languages.

Research experiences

Feb 2024 - July 2024 National Institute of Informatics, Japan.

Research intern, supervised by Prof. Taro Sekiyama. Topic: type-based temporal property verification.

Publications

2024 Zhichao Guan, Yiyuan Cao, Tailai Yu, Ziheng Wang, Di Wang, Zhenjiang Hu, Semantics Lifting for Syntactic Sugar. (accepted to OOPSLA 2024)

2023 Yiyuan Cao, Zhichao Guan, Yushuo Xiao, Haiyan Zhao, Zhenjiang Hu, Development of Domain-specific Languages: Status and Prospects, Science and Technology Foresight, 2023, 2(1): 46-61. (in Chinese)

Teaching

2023 Teaching Assistant. Software Foundations, Peking University, Spring 2023.

Teaching Assistant. Introduction to Functional Programming, Peking University, Fall 2023.

Research projects

Semantics Lifting for Syntactic Sugar.

Syntactic sugar plays a crucial role in engineering programming languages. It offers convenient syntax and higher-level abstractions, as witnessed by its pervasive use in both general-purpose and domain-specific contexts.

Unfortunately, the traditional approach of translating programs containing syntactic sugars into the host language can lead to abstraction leakage, breaking the promise of convenience and hindering program comprehension.

To address this challenge, we introduce the idea of semantics lifting that aims to statically derive self-contained evaluation rules for syntactic sugars. In this way, we get correctly-abstracted semantics for sugar-based DSLs at a low price.

Building Resource-aware Programming Languages in F*. (ongoing)

How well does your program perform? We need more than functional correctness. Resource consumption (e.g., time, memory, and energy) is a crucial aspect of the behavior of programs in real-world applications.

While significant efforts have been made in the domains of automatic resource analysis (e.g., AARA) and manual resource verification (e.g., Separation Logic with time credits) for program resource bounds, there remains a notable gap in the integration of resource consumption information into programming language design.

To address this gap, we are implementing a prototype in F*, a proof-oriented programming language, as a first step towards specifying and verifying resource bounds within a language-integrated framework. One of the key features of our approach is the ability to incorporate existing automatic resource analysis as automatable lemma libraries while retaining the expressiveness and flexibility to specify and verify complex resource bounds with more user intervention.

Proof-integrated System-level Programming Language. (ongoing)

A verification system usually needs three major components: a programming language, a specification language, and a proof language. Can we have a system-level language where programming, specification, and proof seamlessly coexist?

The goal of this project is to merge specification and proof capabilities into a system-level programming language, resulting in more readable specifications that resemble contracts with ghost code and more direct proof manipulation just like programming. This approach has the potential to reduce the needed expertise for doing verification and bridge the communication gaps between proof engineers and program developers, which is often perceived as a significant obstacle to the broader adoption of verification practices.

We are implementing a prototype language C*. We extend the C language with LCF-based proving capabilities and rely on program annotations and symbolic execution to reduce program reasoning to Separation logic entailments.

Resource-aware Temporal Property Verification. (ongoing)

Ensuring the valid use of resources (e.g., a file must be opened before read, a lock must be eventually released) is a critical aspect of program correctness. Previous work in this area either focuses on the verification of general temporal properties (including liveness) of a global trace or handles multiple resource traces but only addresses safety properties.

Our project tries to bridge this gap by presenting a type-based method for the compositional verification of temporal properties of traces generated by each resource. The target language is a higher-order functional language that includes primitives for dynamic resource creation, event-raising, and deallocation.

Awards

2019 China National Scholarship.

Languages

Mandarin Chinese: native.

English: fluent as a working language. (CET-6 score: 607)

Coq: finished Software Foundations Vol. 1, Vol. 2, and most of Vol. 6.

Other languages I speak: C, F*, OCaml, Haskell.