Yiyun Liu

E-mail

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
  POPL’26, draft, coqdoc, rocq proofs (tarball, git)
  
• Consistency of a Dependent Calculus of Indistinguishability
  Yiyun Liu, Jonathan Chan, Stephanie Weirich
  POPL’25, paper, doi, rocq proofs (tarball, git)
  
• Internalizing Indistinguishability with Dependent Types
  Yiyun Liu, Jonathan Chan, Jessica Shi, Stephanie Weirich
  POPL’24, paper, doi, code and rocq proofs (tarball, git)
  
• Dependently-Typed Programming with Logical Equality Reflection
  Yiyun Liu, Stephanie Weirich
  ICFP’23, paper, doi, rocq proofs (tarball, git)
  
• Theoretical Pearl: Short and Mechanized Logical Relation for Dependent Type Theories
  Yiyun Liu, Jonathan Chan, Stephanie Weirich
  unpublished, draft, updated and extended rocq proofs (tarball, git)
  
• A Formal Model of Checked C
  Liyi Li, Yiyun Liu, Deena Postol, Leonidas Lampropoulos, David Van Horn, Michael Hicks
  CSF’22, paper, doi, redex model (tarball)
  
• 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, code (tarball, git)
  

Note: The tarballs are all compressed using zstd. On Mac OS and Linux (or other modern Unix-like systems), simply running tar xvf file.tar.zst should automatically decompress file.tar.zst and unpack its content.

Non-Research Stuff

Here are some developments (mostly mechanized proofs) that are not quite research-level but still somewhat useful.

• Mechanized Parametricity and Normalization for System Fω (git)
• Ltac2 Quickstart Guide (html, git)
• Typed Parallel One Step Reduction (TPOSR) with Autosubst (git)
• An improved and mechanized proof of factorization à la Takahashi (git)
• A helper script that incrementally backups nspawn and incus containers with borg (git)
• Lecture notes about inductive definitions for REPL25 (draft)
  (Note: I’m quite happy with my way of bootstrapping inductive definitions and introducing induction principles, but the notes are otherwise incomplete.)

Changelog

• 2025-11-18: Added missing artifact links and gave the option to download the compressed tarballs directly. Note that while some git links point to my self-hosted git server, you should feel free to clone and fork them on github. My plan is to eventually mirror all the public repos on my private git server to github.