Séminaire, 13 octobre 2011
Lieu
La rencontre aura lieu à l'École Normale Supérieure de Lyon, campus Jacques Monod, dans l'amphi B. Pour venir, voir les instructions sur le site du LIP ou sur un plan, par exemple chez Google Maps. À l'entrée, se présenter à la réception, qui aura la liste des inscrits.
Programme
- 10:30 – 12:00
-
Lorenzo Tortora de Falco (Rome 3)
Following a previous joint work with Daniel de Carvalho and Michele Pagani, we present a semantic approach to the well-known properties of cut-elimination of Linear Logic proof-nets (weak and strong normalization, confluence). This is a joint ongoing work with Daniel de Carvalho.
- 14:00 – 15:00
-
Thomas Braibant (INRIA Grenoble)
We propose a new library to model and verify hardware circuits in the Coq proof assistant. This library allows one to easily build circuits by following the usual pen-and-paper diagrams. We define a deep-embedding: we use a (dependently typed) data-type that models the architecture of circuits, and a meaning function. We propose tactics that ease the reasoning about the behavior of the circuits, and we demonstrate that our approach is practicable by proving the correctness of various circuits: a text-book divide and conquer adder of parametric size, some higher-order combinators of circuits, and some sequential circuits: a buffer, and a register.
- 15:30 – 16:30
-
Agathe Chollet (IML, Marseille) et Laurent Fuchs (XLIM-SIC, Poitiers)
La représentation d'objets géométriques en informatique graphique sépare la structure (topologie, relations d'incidence, d'adjacence) d'un objet et la forme géométrique d'un objet. Pour cette dernière, lors du calcul de la forme géométrique, les résultats des calculs géométriques dépendent très fortement du système numérique utilisé. Cela est principalement du à la nature du résultat à obtenir (un point appartient-il à une droite?) qui, contrairement aux résultats en analyse numérique, ne peut pas se contenter d'une approximation. Différents modèles de calculs, plus ou moins adaptés aux calculs géométriques, ont été proposés et tous n'ont pas des bases théoriques solides. Notre approche se situe dans le cadre de la géométrie discrète dont le principe est d'étudier une version discrétisée d'objets continus. Nous proposons une méthode de discrétisation, l'arithmétisation, fondée sur un modèle discret du système des nombres réels, la droite de Harthong-Reeb.
