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.
Reasoning about the garden of forking paths. Formal reasoning about the cost of lazy programs. (arxiv preprint, under submission at ICFP 2021)
InteractionTrees: program semantics with free monads in Coq.
DeepSpec Web Server (description)
Bidirectional programming with monadic profunctors.
QuickChick: random testing in Coq.
Lysxia on Github.
I have a blog.
Slides on equality (Google Slides)
Slides on algebraic data types (Google Slides)
generic-random: a library of generic random generators.
generic-data: utilities for GHC Generics.