COFIN “LEVI”

This project was about formal techniques for the specification, analysis, verification, synthesis and transformation of software systems. In particular, I was working on logical frameworks, proof assistants and advanced encoding techniques. Some results of that project were the Weak HOAS approach, the Theory of Contexts, the encoding of π-calculus in Coq using these techniques, etc.