Yiyun Liu
- 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
- Algorithmic Conversion with Surjective Pairing: A Syntactic and
Untyped Approach
Yiyun Liu, Stephanie Weirich
under submission, draft
- Consistency of a Dependent Calculus of Indistinguishability
Yiyun Liu, Jonathan Chan, Stephanie Weirich
POPL’25, paper, doi
- Internalizing Indistinguishability with Dependent Types
Yiyun Liu, Jonathan Chan, Jessica Shi, Stephanie Weirich
POPL’24, paper, doi
- Dependently-Typed Programming with Logical Equality Reflection
Yiyun Liu, Stephanie Weirich
ICFP’23, paper, doi
- Theoretical Pearl: Short and Mechanized Logical Relation for
Dependent Type Theories
Yiyun Liu, Jonathan Chan, Stephanie Weirich
unpublished, draft
- A Formal Model of Checked C
Liyi Li, Yiyun Liu, Deena Postol, Leonidas Lampropoulos, David Van Horn, Michael Hicks
CSF’22, paper, doi
- Verifying Replicated Data Types with Typeclass Refinements in Liquid
Haskell
Yiyun Liu, James Parker, Patrick Redmond, Lindsey Kuper, Michael Hicks, Niki Vazou
OOPSLA’20, paper, doi