Li-yao XIA

I’m a PhD student at the University of Pennsylvania since 2017.

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. One project in the DeepSpec expedition is to create a web server that is fully verified down to RTL. I am part of the group working on the application level (on top of sockets and/or HTTP).

• 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

• QuickChick: random testing in Coq.

• InteractionTrees: free monads and algebraic effects in Coq.

• DeepSpec Web Server (description)

• Bidirectional programming with monadic profunctors.

Personal projects

Lysxia on Github.

I have a blog. Sometimes I also write in French.

• The Advent of Code in Coq (https://adventofcode.com/).

• first-class-families: Haskell type families can be made first-class, see my blog post.

• generic-data: utilities for GHC Generics.

• generic-random: a library of generic random generators.

• metamorph: monomorphize polymorphic values, based on the paper Testing Polymorphic Properties.

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)