Li-yao XIA

I’m a post-doc at the University of Edinburgh since 2022, on a project to combine algebraic effects and gradual types.

My main areas of interest are functional programming (Haskell, Coq, Agda), formal verification, and testing. I did my PhD thesis at the University of Pennsylvania, in the PLClub, on interaction trees and their applications to program semantics.

Projects, publications

Google Scholar

Executable Semantics with Interaction Trees. Thesis. (draft, Google slides)
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)
Bidirectional programming with monadic profunctors.
- Composing Bidirectional Programs Monadically, Li-yao Xia, Dominic Orchard, Meng Wang. ESOP 2019. (arxiv, slides.pdf)
QuickChick: random testing in Coq.

Roles

PC Chair for BX 2022

Personal projects

Lysxia on Github.

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.
The Advent of Code in Coq (https://adventofcode.com/).

Maintainerships
- Coq (coqdoc maintainer)
- QuickChick
- haskell/aeson
- haskell/text