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

Google Scholar

• 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.

Personal projects

Lysxia on Github.

I have a blog.

PLClub Talks

• Slides on operational, denotational semantics, full abstraction, game semantics (Google Slides)

• Slides on equality (Google Slides)

• Slides on algebraic data types (Google Slides)

• Slides on 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)
  • 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)