Category: Seminars

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.

Apr 30 2013

Séminaire Marelle : Introduction to homotopy type theory

On Tuesday 30/04/2013, at 10h, in room Byron Blanc.

Speaker: Yves Bertot.

Title: Introduction to homotopy type theory.

Abstract:
Homotopy theory is an offspring of algebraic topology that makes it possible to sort topological spaces in equivalence classes and to study their algebraic properties. Since 2006, connections have been discovered between this theory and type theory, more precisely with respect types used to represent equality.

In this talk, I will describe some of these connection and show how new kinds of data-structures, called higher inductive types start to have a meaning in this context, and how they can be simulated in a simple extension of the Coq system.

Mar 19 2013

Séminaire Marelle : Ordinaux et récursivité

Sorry, this entry is only available in French.

Feb 18 2013

Séminaire Marelle : Du lemme de Hensel aux certificats ISValP

Sorry, this entry is only available in French.

Jan 29 2013

Séminaire Marelle : Forme normale de Frobenius et de Jordan d’une matrice

Sorry, this entry is only available in French.

Aug 09 2012

Séminaire Marelle : Vérification automatique de propriétés de “differential privacy”

Sorry, this entry is only available in French.

Dec 16 2011

Séminaire Marelle : An Introduction to F*, a new dependently typed language for secure distributed programming

On Friday 16/12/2011, at 14h, in room Euler Violet.

Speaker: Pierre-Yves Strub.

Title: An Introduction to F*, a new dependently typed language for secure distributed programming.

Abstract:
Distributed applications are difficult to program reliably and securely. Dependently typed functional languages promise to prevent broad classes of errors and vulnerabilities, and to enable program verification to proceed side-by-side with development. However, as recursion, effects, and rich libraries are added, using types to reason about programs, specifications, and proofs becomes challenging.

I will present F*, a full-fledged design and implementation of a new dependently typed language for secure distributed programming. It’s designed to be enable the construction and communication of proofs of program properties and of properties of a program’s environment in a verifiably secure way.

F* provides arbitrary recursion while maintaining a logically consistent core; it enables modular reasoning about state and other effects using affine types; and it supports proofs of refinement properties using a mixture of cryptographic evidence and logical proof terms.

F* compiles to .NET bytecode in type-preserving style, and interoperates smoothly with other .NET languages, including F#, on which it is based.

Dec 07 2010

Séminaire Marelle : Mixed induction and coinduction

On Tuesday 07/12/2010, at 10h30, in room Byron Blanc.

Speaker: Yves Bertot.

Title: Mixed induction and coinduction.

Abstract:
Several experiments show that data-types where one mixes co-induction and induction can be useful for programming. In particular, this makes it possible to describe the productivity of some algorithms that do not satisfy the coinduction guardedness criterion enforced by the Coq system. In this talk, we will concentrate on a particular description of the Fibonacci sequence, which is semantically well-formed, but which does not satisfy the guardedness criterion, and we will show how this sequence can be modeled using a mix of plain Coq co-recursion and recursion on an ad-hoc inductive predicate.

Nov 30 2010

Séminaire Marelle : L’axiome d’univalence de Voevodsky et l’extensionnalité.

Sorry, this entry is only available in French.

Nov 16 2010

Séminaire Marelle : Vérification formelle pour les méthodes numériques

Sorry, this entry is only available in French.