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.