This is a semester project done in the Spring semester of 2020/2021 in the LAMP laboratory at the EPFL under supervision of Fengyun Liu and Nicolas Stucki.
Its goal was to create a mechanized proof of soundness of calculus defined in A Theory of Quoted Code Patterns which is a formalization of pattern matching on code available in Scala 3 as part of its new macro system.
The mechanization in the Coq proof assistant can be found in the calculus/ directory.
It uses Coq version 8.9.1 and DbLib library.
The report of the semester project is available at report.pdf.
The examples/ directory contains some examples from the report.
The semester project was presented at 18.06.2020. Slides with notes from the presentation are available in presentation_notes.pdf.