In this project we attempt to fully implement the "Applicative Matching Logic" framework in Coq, with example intances.
CoqIDE 8.11.0 https://coq.inria.fr/download
Official language definition http://fsl.cs.illinois.edu/index.php/Applicative_Matching_Logic
Snapshot version of the technical report, that was used for the ipmlementation can be found in doc\chen-rosu-2019-trb-public_march182020.pdf