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.
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.
DeepSpec Web Server (description)
Bidirectional programming with monadic profunctors.
QuickChick: random testing in Coq.
- PC Chair for BX 2022
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)
generic-random: a library of generic random generators.
generic-data: utilities for GHC Generics.