Li-yao XIA
I’m a PhD student at the University of Pennsylvania since 2017, in the PLClub.
My main topic of interest is program correctness via the design of languages (in a broad sense encompassing libraries and programming patterns) that facilitate programming, specification, and verification.
Formal verification. I am interested in techniques to model and verify programs, mainly using the Coq proof assistant. The DeepSpec expedition aims to verify whole systems from application to transistors.
Testing. Either in combination with or as an alternative to formal verification. I am particularly interested in random testing (e.g., with QuickCheck in Haskell, QuickChick in Coq) and related techniques (e.g., enumerative testing).
Type systems, parametricity, denotational semantics. Ways to guarantee invariants by construction.
Type-driven programming. Types do more than just providing safety. They can also guide programming as an activity. Some programs can even be derived from types to a large extent, for example via generic programming.
Other interests: algorithms, combinatorics, abstract nonsense.
Projects, publications
Executable Semantics with Interaction Trees. Thesis. (draft)
C4: Verified Transactional Objects. Mohsen Lesani, Li-yao Xia, Anders Kaseorg, Christian J. Bell, Adam Chlipala, Benjamin C. Pierce, Steve Zdancewic. OOPSLA 2022. (PDF, Coq artifact on Zenodo)
Reasoning about the garden of forking paths. Yao Li, Li-yao Xia, Stephanie Weirich. ICFP 2021. (arxiv preprint)
InteractionTrees: program semantics with free monads in Coq.
- Interaction Trees: Representing Effectful and Recursive Programs in Coq. Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, Steve Zdancewic. POPL 2020. (arxiv, talk, conference page with links to slides)
DeepSpec Web Server (description)
- From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server.
Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia,
Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, Steve Zdancewic.
CPP 2019.
(arxiv,
slides.pptx,slides.pdf, talk transcript)
- From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server.
Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia,
Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, Steve Zdancewic.
CPP 2019.
(arxiv,
Bidirectional programming with monadic profunctors.
- Composing Bidirectional Programs Monadically,
Li-yao Xia, Dominic Orchard, Meng Wang. ESOP 2019.
(arxiv,
slides.pdf)
- Composing Bidirectional Programs Monadically,
Li-yao Xia, Dominic Orchard, Meng Wang. ESOP 2019.
(arxiv,
QuickChick: random testing in Coq.
Personal projects
I have a blog.
PLClub Talks (slides)
Seeing the World through Lenses (Google Slides)
From Operational to Denotational Semantics: Full Abstraction and Game Semantics (Google Slides)
A Garden Path towards Equality (Google Slides)
Algebraic Data Types (Google Slides)
Defunctionalization (Google Slides, PDF).
Programming, Libraries
first-class-families: Haskell type families can be made first-class, see my blog post.
generic-random: a library of generic random generators.
generic-data: utilities for GHC Generics.
metamorph: monomorphize polymorphic values, based on the paper Testing Polymorphic Properties.
Maintainerships
- Coq (coqdoc maintainer)
- haskell/aeson
- haskell/text
Past activities
Links
Prologin, a programming contest for French teenagers. I was a member of the organizing association in 2016.
dissemin, an open source website helping researchers to spot and release their paywalled papers. (Python)