Vous pouvez vous abonner à nos annonces de séminaires
http://gallium.inria.fr/seminaires/
S E M I N A I R E
__
/ _` _ / / o
/ ) __) / / / / / /\/|
(___/ (_/ (_ (_ / (__/ / |
I N R I A - Paris
2 rue Simone Iff (ou: 41 rue du Charolais)
Salle Lions 2, bâtiment C
Lundi 15 mai, 11h00
--------------
Cyprien Mangin
--------------
Université Paris Diderot
======================================================
Equations: a tool for programming with dependent types
======================================================
Dependent types are a part of what makes a proof assistant such as Coq a
useful tool, and yet programming with them often raises some difficulties.
Equations is a tool that aims at making this process easier, by bridging the
gap between what we, as users, want to write, and what the Coq kernel will
accept as a valid proof term. In this presentation, we will first recall what
are dependent types and what are those difficulties and follow with a
comprehensive description of the main algorithm behind Equations. The rest of
the talk will focus on the concrete usage of Equations and several examples to
showcase the different features it offers.