Projects
Here is a list of projects I’ve worked on and contributed to in the past 5 years or so. Mostly related to type theory, computational logic and formal methods.
Large-scale/work projects
- A partial commutative monoid library in Coq
- Hoare Type Theory
- Fine-grained concurrent separation logic
- LiquidHaskell
Personal projects
- A port of the “Functional Data Structures and Algorithms” books into Coq/SSReflect
- Formalizations of various computational sequent calculi and abstract machines
- Some modal type theories
- Calculi of constructive refutation
Guarded types
- A Cubical Agda library for working with guarded type theory
- Some formalizations of automata in guarded TT
- Tricky proofs of termination via guarded TT
- Experiments with the logical relations method in guarded TT
Automated reasoning
- An updated version of Weich’s IPC proof search engine
- Formalizations of propositional automated reasoning methods
- Formalized abstract interpretation