ERC SECOMP - Efficient Formally Secure Compilation to a Tagged Architecture
Description: I am an R&D Engineer at Inria. I like to build bridges between state-of-the-art research and industry.
cloud (8088) about (3918) coq (30)
I am an R&D Engineer at Inria. I like to build bridges between state-of-the-art research and industry.
Coq is a fascinating piece of open-source software, that makes it possible to prove the correctness of programs or mechanically formalize the proof of mathematical theorems. Have a look at Coq’s website .
I work on improving and promoting the Coq proof assistant, and on building a Consortium of academic and industrial users of Coq. If you want to know more, don’t hesitate to contact me .
ERC SECOMP - Efficient Formally Secure Compilation to a Tagged Architecture