Yiyun Liu

E-mail
liuyiyun@seas.upenn.edu
Bluesky
Yiyun Liu@electriclam.com
Matrix
@ohqo:electriclam.com
Blog
blog.electriclam.com
Git
forgejo, yiyunliu@github

I am a final year CS PhD student at the University of Pennsylvania, advised by Prof. Stephanie Weirich. My current research is about how dependently typed programming languages and dependency tracking can benefit from each other.

I spend a lot of my time working in the Rocq proof assistant: I mechanize all my correctness proofs, from syntactic type soundness to semantic logical consistency. And I look for ways to make such proofs as streamlined as possible, so we can be more confident about the design of our systems while still being productive at exploring new features.

I got my MS degree from the University of Maryland, advised by Prof. Michael Hicks. My research involved formal verification of replicated data types, random testing, and modeling of CheckedC in Redex.

Research