2025-01-05 17:24:58 -05:00
* Yiyun Liu
- E-mail :: [[mailto:liuyiyun@seas.upenn.edu ][liuyiyun@seas.upenn.edu ]]
2025-01-05 19:13:43 -05:00
- Social :: [[https://bsky.app/profile/ohqo.bsky.social ][ohqo.bsky.social@Bluesky ]]
2025-01-05 17:24:58 -05:00
- Blog :: [[https://blog.electriclam.com ][blog.electriclam.com ]]
- Github :: [[https://github.com/yiyunliu ][yiyunliu ]]
I am currently a fourth-year CS PhD student at University of
Pennsylvania, advised by [[https://www.seas.upenn.edu/~sweirich/ ][Prof. Stephanie Weirich ]]. I got my MS degree from University of Maryland, advised
by [[https://www.cs.umd.edu/~mwh/ ][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* , [[file:papers/dcoiomega.pdf ][paper ]]) ::
*Yiyun Liu* , Jonathan Chan, Stephanie Weirich
- Theoretical Pearl: Short and Mechanized Logical Relation for Dependent Type Theories (Unpublished, [[file:papers/mltt.pdf ][draft ]]) ::
*Yiyun Liu* , Jonathan Chan, Stephanie Weirich
- Internalizing Indistinguishability with Dependent Types (*POPL24* , [[file:papers/dcoi.pdf ][paper ]]) ::
*Yiyun Liu* , Jonathan Chan, Jessica Shi, Stephanie Weirich
2025-01-05 19:13:43 -05:00
- Dependently-Typed Programming with Logical Equality Reflection
(*ICFP23* , [[file:papers/systemde.pdf ][paper ]], [[https://doi.org/10.1145/3607852 ][doi ]]) ::
2025-01-05 17:24:58 -05:00
*Yiyun Liu* , Stephanie Weirich
2025-01-05 19:13:43 -05:00
- A Formal Model of Checked C (*CSF22* , [[file:papers/checkedc.pdf ][paper ]], [[https://doi.ieeecomputersociety.org/10.1109/CSF54842.2022.9919657 ][doi ]]) ::
2025-01-05 17:24:58 -05:00
Liyi Li, *Yiyun Liu* , Deena Postol, Leonidas Lampropoulos, David Van Horn, Michael Hicks
2025-01-05 19:13:43 -05:00
- Verifying Replicated Data Types with Typeclass Refinements in Liquid
Haskell (*OOPSLA20* , [[file:papers/vrdt.pdf ][paper ]], [[https://doi.org/10.1145/3428284 ][doi ]]) ::
2025-01-05 17:24:58 -05:00
*Yiyun Liu* , James Parker, Patrick Redmond, Lindsey Kuper, Michael Hicks, Niki Vazou
