Séminaire le 11 février 2010

Streams represent discrete potentially infinite information flows, this is one of the reasons of their ubiquity in modern computer and information science. Developing new languages and tools for the design and the analysis of stream programs is of great importance. In this talk, I propose some logical and semantic techniques and tools to model and to analyze stream programs.

Les structures algébriques doivent parfois être typées. Par exemple, les matrices sur des nombres réels forment un anneau, mais la multiplication est seulement une opération partielle: les dimensions doivent concorder. Une façon naturelle de considérer les matrices de façon algébrique consiste à travailler avec des «anneaux typés». Nous prouvons plusieurs théorèmes de «détypage»: dans certaines algèbres (semi-anneaux, algèbres de Kleene, treillis résidués, treillis résidués involutifs), les équations typées peuvent être dérivées à partir des équations non typées sous-jacentes. Les procédures de décision non typées correspondantes peuvent ainsi être étendues directement aux structures typées. Certains de ces théorèmes sont obtenus par un détour à propos de fragments de la logique linéaire cyclique.