Sites Inria

There are 1 Results with the keyword : "Horizon2020"

Nicolas Tabareau

European Research Council 2014

Democratizing Proof Assistants

Jean-Michel Prima - 10/02/2015

Proving theorem and software correctness are the two raisons d'être of proof assistants. Coq, the result of a 25-year project driven by Inria, has become a preeminent tool in this domain. Yet, a recent breakthrough in mathematics by Fields medal Vladimir Voevosdky has opened the door to a huge improvement of formal verification. Inria scientist Nicolas Tabareau is being granted funding by the European Research Council (ERC) in order to explore how this finding could indeed pave the way to a novel and much enhanced version of Coq. As he explains, this work is expected to have a very strong impact and spread the use of this proof assistant across the industry.

Keywords:

Home > Centre > Rennes > News > Nicolas Tabareau : démocratiser les assistants de preuve

More

Top