Section: Overall Objectives

Highlights of the Year

• The Castor informatiquehttp://castor-informatique.fr/ , is an international competition to present computer science to pupils (from 6ème to terminale). More than 170,000 teenagers played on more than 30 proposed exercises in November 2013. Two members of the Toccata team (S. Boldo and A. Charguéraud) belong to the organization committee (5 people).

• The full formalization of the JavaScript language specification (ECMAScript 5) was recently completed by the JsCert team [24] , which includes A. Charguéraud and 7 collaborators from Imperial College and Inria Rennes (http://jscert.org ). The formalization, which involves more than 10,000 lines of code and an inductive semantics with over 600 reduction rules, is the result of 2 years of effort. It lead to the discovery of bugs in the official standard, in the official test suites, and in all major browsers. In particular, it has raised the interest of several members of the ECMAScript standardization committee, and that of the developers of secure subsets for JavaScript.

• J.-C. Filliâtre was invited as keynote speaker (“One Logic To Use Them All” [19] ) at the International Conference on Automated Deduction in 2013. It is the main conference of the year in the domain of Automated Reasoning. In this talk he presented the Why3 approach for interacting with dozens of provers on the same theories and goals. This invited talk is a recognition by the community of this unique feature of Why3.

• Most 18-year old French students pass an exam called Baccalaureate which ends the high school and is required for attending the university. The idea was to try our Coq library Coquelicot on the 2013 mathematics test of the scientific Baccalaureate. C. Lelay went to the “Parc de Vilgénis” high school in Massy, France and took the 2013 test at the same time as the students, but had to formally prove the answers [45] (see also https://www.lri.fr/~lelay/ ).

• The Coq proof assistant received the ACM Programming Languages Software Award in 2013 http://www.sigplan.org/Awards/Software/Main . The development of Coq was initiated by Thierry Coquand and Gérard Huet in 1984. The current environment is the result of the work of more than 40 direct contributors, including major contributions by Christine Paulin-Mohring and Jean-Christophe Filliâtre from our team.