41 lines
2.3 KiB
Org Mode
41 lines
2.3 KiB
Org Mode
|
* Yiyun Liu
|
||
|
|
- E-mail :: [[mailto:liuyiyun@seas.upenn.edu][liuyiyun@seas.upenn.edu]]
|
||
|
|
- Social :: [[https://bsky.app/profile/ohqo.bsky.social][ohqo.bsky.social@BluesKy]]
|
||
|
|
- 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
|
||
|
|
|
||
|
|
- Dependently-Typed Programming with Logical Equality Reflection (*ICFP23*, [[file:papers/systemde.pdf][paper]],[[https://doi.org/10.1145/3607852][doi]]) ::
|
||
|
|
*Yiyun Liu*, Stephanie Weirich
|
||
|
|
|
||
|
|
- A Formal Model of Checked C (*CSF22*, [[file:papers/checkedc.pdf][paper]],[[https://doi.ieeecomputersociety.org/10.1109/CSF54842.2022.9919657][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*, [[file:papers/vrdt.pdf][paper]],[[https://doi.org/10.1145/3428284][doi]]) ::
|
||
|
|
*Yiyun Liu*, James Parker, Patrick Redmond, Lindsey Kuper, Michael Hicks, Niki Vazou
|