FORTissimo: Automating the First-Order Theory of Rewriting
In the FORTissimo project, I have formalized constructions involving ground tree transducers (GTTs) and regular relations (RRn relations) in Isabelle/HOL.
From Confluence to Unique Normal Forms: Certification and Complexity
This project is almost complete.
I have worked on the Confluence and Unique Normal Forms project.
This involved both extending our confluence prover, CSI, and formalizing results in IsaFoR for integration in the CeTA certifier.
Automating Confluence
This project has been completed.
As part of the Confluence Project, I investigated and implemented criteria for proving confluence of term rewrite systems.