About Me

I’m currently a third-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.

I also invested a lot of time on music production, though I still haven’t managed to get more than 100 clicks on my Soundcloud.

Github

https://github.com/yiyunliu