Yves BERTOT

Author's posts

Oct 31 2017

Two new winter schools on Coq

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.

Apr 05 2014

Thesis defense: Interaction between linear algebra and topology in formalized mathematics

2014-04-04

Nov 22 2013

Séminaire Marelle : A Coq formalization of finitely presented modules.

On Friday 22/11/2013, at 10h30, in room Byron Beige,

Speaker: Cyril Cohen.
Joint work with: Anders Mortberg.

Title: A Coq formalization of finitely presented modules.

Abstract:
The use of vector spaces in homology theory does not give as precise
information as with modules. A generalization to finitely presented modules
covers computable Z-homology, which gives finer-grained topological invariants.
We formalize a construction of finitely presented modules over coherent and
strongly discrete rings and discuss its properties. This formalization gives
basic building blocks that lead to a clean definition of homology groups.

Nov 20 2013

Soutenance de Thèse : Étude formelle d’algorithmes efficaces en algèbre linéaire

Sorry, this entry is only available in French.

Nov 20 2013

Séminaire Marelle : Types and Data types in Continuation Calculus and lambda calculus

On Wednesday 20/11/2013, at 10h30, in room Byron blanc.

Speaker: Herman Geuvers.
Joint work with: Bram Geron, Universty of Birmingham.

Title: Types and Data types in Continuation Calculus and lambda calculus.

Abstract: Continuation Calculus (CC), as defined in [1], is a model for functional
computations that aims at (1) being simple (simpler than lambda calculus
and term rewriting), (2) remaining close to actual implementations and
(3) being generic (incorporating various evaluation strategies).
The original system is untyped, but there is a standard procedure for
defining data in CC and writing functions over this data.
In the talk we present a typing system for CC and compare it with the
typing of data in lambda calculus. In lambda calculus, one has the
iterative representation of data (e.g. the Church numerals), but also
the less well-known recursive representation (e.g. the so called “Scott
numerals”). In CC, the recursive data are the “standard” ones and we
show how to type them, compute with them and reason over them.

[1] Bram Geron and Herman Geuvers — Continuation calculus,
Proceedings First Workshop on Control Operators and their Semantics,
2013, edited by: Ugo de’Liguoro and Alexis Saurin, EPTCS 127, pp 66-85.

Aug 26 2013

Séminaire Marelle : Certified, Efficient and Sharp Univariate Taylor Models in COQ.

On Monday 26/08/2013, at 14h30, in room Byron Blanc.

Speaker: Érik Martin-Dorel.

Title: Certified, Efficient and Sharp Univariate Taylor Models in COQ.

Abstract:
We present a formalisation, within the COQ proof assistant, of
univariate Taylor models. This formalisation being executable, we get a
generic library whose correctness has been formally proved and with
which one can effectively compute rigorous and sharp approximations of
univariate functions composed of usual functions such as 1/x, sqrt(x),
exp(x), sin(x) among others. In this talk, we present the key parts of
the formalisation and we evaluate the quality of our certified library
on a set of examples.

Aug 06 2013

Séminaire Marelle : Sur la théorie des types homotopiques

Sorry, this entry is only available in French.

Jul 17 2013

Séminaire Marelle : Automatisation de preuves en Coq par traduction en logique du premier ordre

Sorry, this entry is only available in French.

Jul 08 2013

Séminaire Marelle : Le théorème des trois cercles

Sorry, this entry is only available in French.

Jun 11 2013

Séminaire Marelle : Vérification formelle de certificats fondés sur le lemme de Hensel

Sorry, this entry is only available in French.