The marelle team will organize an advanced school from December 4th to December 8th, 2017 and an introductory school from January 22nd to January 26th, 2017.
Sep 08 2015
Talk by Claudio Sacerdoti Coen
On Thursday 20150924, at 10:30, in room Byron Blanc,
Speaker: Claudio Sacerdoti Coen
Title: On the Relative Usefulness of Fireballs
Publication: Beniamino Accattoli, Claudio Sacerdoti Coen, LICS 2015.
Abstract:
In CSLLICS 2014, Accattoli and Dal Lago showed that there is an implementation of the ordinary (i.e. strong, pure, callbyname) lambdacalculus into models like RAM machines which is polynomial in the number of betasteps, answering a longstanding question. The key ingredient was the use of a calculus with useful sharing, a new notion whose complexity was shown to be polynomial, but whose implementation was not explored. We study useful sharing in a callbyvalue scenario, introducing a new reduction machine to reduce open terms according to callbyvalue and that has only a _LINEAR_ overhead with respect to the number of betasteps.
Jul 09 2015
Talk by Tsvetan Chavdarov Dunchev
On Thursday 20150709, at 10:30, in room F102,
Speaker: Tsvetan Chavdarov Dunchev
Title: Automation of cutelimination in proof schemata
Abstract:
Schematising sets of objects by abstracting their general structure is an important and frequently necessary task in mathematics. In this talk will be presented a method for cutelimination by resolution for propositional and firstorder proof schemata (CERESs). Cutelimination, introduced by Gentzen, is the most prominent form of proof transformation in logic and plays an important role in automating the analysis of mathematical proofs. The removal of cuts corresponds to the elimination of intermediate statements (lemmas) from proofs resulting in a proof which is analytic in the sense, that all statements in the proof are subformulas of the result. Therefore, the proof of a combinatorial statement is converted into a purely combinatorial proof. For a given proof schemata we will extract a (schematic) set of clauses which is always unsatisfiable. A resolution refutation of this set will be constructed using the notion of the resolution schemata. The obtained refutation will be used as a skeleton of a proof in normal form with at most atomic cutformulas.
Jun 11 2015
Talk by Isabella Dramnesc
On Thursday 20150611, at 10h30, in room Byron Blanc,
Speaker: Isabela Drãmnesc
Title: Proofbased Synthesis of Algorithms on Binary Trees
Abstract:
Program synthesis is currently a very active area of programming language and verification communities. We address the problem of synthesizing sorting algorithms operating on binary trees.
We develop several proof techniques by extending our previous work on the synthesis of algorithms on lists. We design appropriate induction principles and various provesolve methods mixing rewriting with assumptionbased forward reasoning and goalbased backward reasoning.
The proof techniques are implemented in the Theorema system and are used for the automatic synthesis of several sorting algorithms and for some auxiliary functions. For some of the synthesized algorithms we check the correctness in the Coq system.
May 22 2015
The Coq Workshop 2015
The 7^{th} Coq Workshop will be held in Sophia Antipolis, France – June 26, 2015.
Jan 29 2015
Marelle Seminar: Proofs as documents: asynchronous interaction for Coq
On Thursday 29/01/2015, at 10h30, in room Byron Blanc,
Speaker: Carst Tankink
Title: Proofs as documents: asynchronous interaction for Coq
Abstract:Since the beginning of interactive theorem proving, the actual interaction has been a simple backandforth between the user and the prover, with the user providing a command the prover eagerly executes, giving feedback the user then uses to compose a new command. I will present a documentoriented model for Coq proofs (based on Wenzel’s PIDE architectures for Isabelle) that asynchronously updates the proof and processes the results from the prover. This model allows faster (parallel) processing of complete proof scripts, supports a simpler interaction model for readers of formal proofs, and gives a cleaner API for writing third party tools working on top of the proof assistant’s results. I will demonstrate the model and the interactions it allows using the jEdit plugin for Coq.
Dec 19 2014
First Coq Coding Sprint – June 2225 2015 SophiaAntipolis
All scientific information : https://coq.inria.fr/cocorico/CoqCodingSprint/CoqCS1
Aug 08 2014
Yves Bertot récompensé par l’ACM Software System Award
Le logiciel Coq est une nouvelle fois récompensé par l’Association for Computing Machinery. ACM Software System Award à San Francisco le 21 juin 2014 Sur la photo, Yves Bertot (2ème sur la gauche) est entouré de quatre des huit autres récipiendaires du Software System Award 2013 :
 Thierry Coquand, Université de Gothenburg;
 Gérard Huet, Inria Paris – Rocquencourt;
 Christine PaulinMohring, Université Paris Sud/Inria Saclay IledeFrance;
 Bruno Barras, Inria Saclay/École Polytechnique;
 JeanChristophe Filliâtre, CNRS/Inria Saclay – IledeFrance;
 Hugo Herbelin, Inria Paris – Rocquencourt;
 Chet Murthy, Google Inc.;
 Yves Bertot, Inria Sophia AntipolisMéditerranée ;
 Pierre Castéran, Université de Bordeaux.
La vidéo de l’évènement (La même sur youtube), la photographie de la remise de prix.
Apr 17 2014
Coq receives the 2013 Software system Award
Coq selected as recipient of the 2013 Software system Award

Coq is a software tool for the interactive development of formal proofs, which is a key enabling technology for certified software. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semiinteractive development of machinechecked proofs. An open source product, Coq has played an influential role in formal methods, programming languages, program verification and formal mathematics. As certification gains importance in academic and industrial arenas, Coq plays a critical role as a primary programming and certification tool. Coq’s first implementation was in 1985, when it was named CoC (the acronym for the logic it implemented: the Calculus of Constructions). This system was developed by the Coq Development Team whose primary members were Thierry Coquand, University of Gothenburg; Gérard Huet, INRIA Paris – Rocquencourt; Christine PaulinMohring, University Paris Sud/INRIA Saclay; Bruno Barras, INRIA Saclay/École Polytechnique; JeanChristophe Filliâtre, CNRS/INRIA Saclay; Hugo Herbelin, INRIA Paris – Rocquencourt; Chet Murthy, Google Inc.; Yves Bertot, INRIA Sophia; and Pierre Castéran, University of Bordeaux.
ACM will present the 2013 Software System Award at its annual Awards Banquet on June 21 in San Francisco, CA.
Apr 05 2014
Thesis defense: Interaction between linear algebra and topology in formalized mathematics
20140404