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.
QuickChick: random testing in Coq.
InteractionTrees: free monads and algebraic effects in Coq.
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)
Bidirectional programming with monadic profunctors.
generic-random: a library of generic random generators.
generic-data: utilities for GHC Generics.