Sites Inria

There are 8 Results with the keyword : "proof"

HACL*

Recherche

HACL*

Team: PROSECCO -

We demonstrate HACL*, a verified cryptographic library written in F* and compiled to C. Verification guarantees that our code is memory safe, functionally correct, and free from integer overflows and certain kinds of side-channel leaks. We rely on Kremlin, a compiler from F* to C with formal correctness guarantees  and on CompCert a verified compiler for C. We demonstrate the usage of our library to build a file transfer application and a reference TLS library.

Keywords:

Home > Centre > Nancy > Innovation > RII 2016 > Demos > HACL*

More

1984

Chronology: Seven Key Dates

Mathilde De Vos -

On 23 January 2013 the Coq program is to receive the SIGPLAN Programming Languages Software Award. This prize is conferred on an annual basis in recognition of a software program that has had a significant impact on research and development in the field of programming languages. Here are seven key dates in the project's history.

Keywords:

Home > Innovation > Research Partnerships & Transfer > COQ > Chronologie

More

Coq: Thirty Years of Teamwork

Julien Thèves, Citizen Press -

Conceived thirty years ago at Inria's Paris-Rocquencourt laboratory, the Coq Proof Assistant continues to mobilise research teams. Its continuous development is a testimony to the interest shown in it by both the scientific community and, more recently, the financial sector.

Keywords:

Home > Innovation > Research Partnerships & Transfer > COQ > 30 ans de travail d’équipe

More

Coq: the Program that Provides the Proof

Julien Thèves, Citizen Press -

The winner of the SIGPLAN1 Programming Languages Software Award in January 2014, the Coq program has provided invaluable support for nearly thirty years now for computer scientists who use it as an aid for writing and checking programs. This extremely efficient proof assistant has won over numerous mathematicians too.

Keywords:

Home > Innovation > Research Partnerships & Transfer > COQ > La preuve par le logiciel

More

Rewriting theory

International School on Rewriting

1/07/2019 to 6/07/2019

The 11th edition of the International School on Rewriting will be held from 1 to 6 July 2019 in Paris. Organized by Inria and MINES ParisTech, it is intended for Master and PhD students as well as researchers interested in the study of rewriting concepts and their application.

Place : MINES ParisTech

Keywords:

Home > Centre > Saclay > Calendar > École internationale d'été en réécriture

lire la suite

© Photo Bernard Lachaud

Computer-assisted proof

Mathematical proof by computer science!

Nathaly Mermet - 22/11/2012

A complete formal proof, certified by the Coq software, was announced in September by Georges Gonthier and his team at the Inria-Microsoft Research joint laboratory.

This work renders the conflict between computer science and mathematics obsolete, the common denominator being logic. Two young researchers who joined Georges Gonthier for the ride told us how much they enjoyed participating in the work and "grew" as a result of the Mathematical Components (MathComp) project. Here's what they had to say...

Keywords:

Home > Research > News > La preuve mathématique par informatique !

More

Georges Gonthier, join laboratory Microsoft Research-Inria © Laboratoire commun Inria-Microsoft Research

Computer-assisted proof

"Our work diagram looked like a Napoleonic war plan!"

Françoise Breton - 22/11/2012

Six years transpired between the start of the project and the end of the proof of the Feit-Thompson theorem, which came on 20 September 2012. Following is the account of this modern-day adventure.

Interview with Georges Gonthier, Microsoft Research-Inria joint laboratory.

Keywords:

Home > Research > News > Georges Gonthier : Notre diagramme de travail ressemblait à un plan de guerre napoléonienne !

More

© Inria / Photo Kaksonen

Computer-assisted proof

A major success for computer-assisted proof

Françoise Breton - 22/11/2012

Six years after the computer-assisted proof of the four colour theorem, Georges Gonthier and his team have successfully proven the far more complex Feit-Thompson theorem, a central theorem in group theory and group classification. This is a significant step forward for mathematicians, who are increasingly utilising computer-assisted proof. Moreover, it is a success for computer science, which as a result of this endeavour has shown its ability to deploy advanced tools and techniques to codify mathematics.

Keywords:

Home > Research > News > Un grand succès pour la preuve informatique

More

Top