Yves BERTOT
Author's posts
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 12 2012
MAP 2012 – International Spring School on Formalization of Mathematics
Event: International Spring School on Formalization of Mathematics – MAP 2012.
Date: March 12–16, 2012.
Location: Sophia Antipolis, France.
Website: http://www-sop.inria.fr/manifestations/MapSpringSchool/
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.
