The project develops a formal definition of matching logic in the Coq proof assistant, allowing us to prove meta-theorems and theorems in matching logic in a machine-checkable way.

The project aims at developing a formal semantics and formal program equivalence definitions for the Erlang programming language, mechanized in the Coq proof assistant.

Static and dynamic verification of program refactoring by using formal methods.