Yiyun Liu
- liuyiyun@seas.upenn.edu
- Bluesky
- Yiyun Liu@electriclam.com
- Blog
- blog.electriclam.com
- Git
- yiyunliu@github, forgejo
I am currently a fourth-year CS PhD student at University of Pennsylvania, advised by Prof. Stephanie Weirich. I got my MS degree from University of Maryland, advised by Prof. Michael Hicks.
My current research is about integrating dependently typed programming languages and graded type systems. I investigate how dependent types and grades can benefit from each other. I mechanize all my correctness proofs, from syntactic type soundness to semantic logical consistency. I’m looking 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.
My past research involves formal verification of replicated data types, random testing, and modeling of CheckedC in Redex.
Research
- Consistency of a Dependent Calculus of Indistinguishability (POPL25, paper, doi)
-
Yiyun Liu, Jonathan Chan, Stephanie Weirich
- Theoretical Pearl: Short and Mechanized Logical Relation for Dependent Type Theories (Unpublished, draft)
-
Yiyun Liu, Jonathan Chan, Stephanie Weirich
- Internalizing Indistinguishability with Dependent Types (POPL24, paper)
-
Yiyun Liu, Jonathan Chan, Jessica Shi, Stephanie Weirich
- Dependently-Typed Programming with Logical Equality Reflection (ICFP23, paper, doi)
-
Yiyun Liu, Stephanie Weirich
- A Formal Model of Checked C (CSF22, paper, doi)
-
Liyi Li, Yiyun Liu, Deena Postol, Leonidas Lampropoulos, David Van Horn, Michael Hicks
- Verifying Replicated Data Types with Typeclass Refinements in Liquid Haskell (OOPSLA20, paper, doi)
- Yiyun Liu, James Parker, Patrick Redmond, Lindsey Kuper, Michael Hicks, Niki Vazou