We design and implement trustworthy software tools (such as refactorings and compilers) for functional programming languages, primarily by using formal methods (proof assistants like Rocq), and novel methods for testing. Our case study language is Erlang. Besides, we also work on the Rocq formalisation of various formal theories, including variants of matching logic, and corresponding metatheories.
- Core Erlang mechanized in Rocq
- Applicative Matching Logic mechanized in Rocq
- Property-based testing of Erlang formal semantics
- Property-based testing of Erlang program equivalence
- TBD