sp-eta-postpone
Rocq formalization accompanying “Algorithmic Conversion with Surjective Pairing” (POPL 2026).
People
Yiyun Liu
Research Scientist
Yiyun Liu is a research scientist at Basis working on type theory and formal verification. His PhD work with Stephanie Weirich at the University of Pennsylvania designed dependent type systems and mechanized their correctness properties in the Rocq proof assistant, with publications at POPL, ICFP, OOPSLA, and CSF.
About
I am a research scientist at Basis. I recently completed my PhD at the University of Pennsylvania under Stephanie Weirich. Before that, I received my MS from the University of Maryland under Michael Hicks.
My research broadly involves designing type systems and formalizing their correctness properties. I work on mechanized proofs in the Rocq proof assistant—covering syntactic type soundness and semantic consistency—and look for ways to make such proofs as streamlined as possible.
Software
Mechanized formalizations and research code.
mltt-consistency
A short, mechanized logical relation for dependent type theories.
Recent Publications
Recent papers and preprints.
Algorithmic Conversion with Surjective Pairing
Y. Liu, Stephanie Weirich
Consistency of a Dependent Calculus of Indistinguishability
Y. Liu, Jonathan Chan, Stephanie Weirich
Internalizing Indistinguishability with Dependent Types
Y. Liu, Jonathan Chan, Jessica Shi, Stephanie Weirich
Dependently-Typed Programming with Logical Equality Reflection
Y. Liu, Stephanie Weirich
Selected Publications
Earlier selected work.
A Formal Model of Checked C
Liyi Li, Y. Liu, Deena Postol, Leonidas Lampropoulos, David Van Horn, Michael Hicks
Verifying Replicated Data Types with Typeclass Refinements in Liquid Haskell
Y. Liu, James Parker, Patrick Redmond, Lindsey Kuper, Michael Hicks, Niki Vazou