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.

Oct 11 2010

Séminaire Marelle : La vérification formelle du théorème de Perron-Frobenius

Sorry, this entry is only available in French.

Sep 09 2010

Séminaire Marelle : Formaliser des fonctions polynomiales en Coq

Sorry, this entry is only available in French.

Jul 08 2010

Séminaire Marelle : A combination of a dynamic geometry software with a proof assistant for interactive formal proofs

On Thursday 08/07/2010, at 11h, in room Byron Blanc.

Speaker: Tuan-Minh Pham.

Title: A combination of a dynamic geometry software with a proof assistant for interactive formal proofs.

Abstract:
This paper presents an interface for geometry proving. It is a combination of a dynamic geometry software, Geogebra[11] with a proof assistant, Coq[8]. Thanks to the features of Geogebra, users can create and manipulate geometric constructions, they discover conjectures and interactively build formal proofs with the support of Coq. Our system allows users to construct fully traditional proofs in the same style as the ones in high school. For each step of proving, we provide a set of applicable rules verified in Coq for users, we also provide tactics in Coq by which minor steps of reasoning are solved automatically.

Jun 30 2010

Séminaire Marelle : De SAT à SMT

Sorry, this entry is only available in French.

Jun 25 2010

Séminaire Marelle : Formalisation du lemme de Hensel en Coq

Sorry, this entry is only available in French.

Jun 09 2010

Séminaire Marelle : Effective and sequential definition by cases on the reals via infinite signed-digit numerals by M. Escardo

Sorry, this entry is only available in French.