Parisian Master of Research in Computer Science
Master Parisien de Recherche en Informatique (MPRI)

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

cours:c-2-21 [2011/07/12 19:26] (current)
Line 1: Line 1:
 +
 +===== Calculs algébriques et fonctionnels =====
 +
 +Resp.: G. Huet, D. Kesner
 +
 +==== Objectifs ====
 +
 +La réécriture repose sur l'idée de manipuler et de transformer
 +des expressions, des valeurs, des propriétés et des méthodes. 
 +Les paradigmes de programmation fonctionnels, logiques,
 +équationnels, par réécriture et orientés objets aussi bien que
 +les langages concurrents et les assistants à la démonstration sont
 +modélisés par ce type de transformations. La réécriture est
 +aussi utilisée dans le raisonnement logique et mathématique, la
 +spécification de protocoles de sécurité et de méthodes de
 +résolution de contraintes, les systèmes de transition, les
 +langages naturels, la sémantique opérationnelle, les
 +spécifications algébriques, la transformation de programmes,
 +...
 +
 +Ce cours propose une vision générale sur la réécriture de termes en
 +mettant l'accent sur les motivations, les techniques et les
 +applications de ces systèmes. On s'intéressera aux propriétés
 +syntaxiques fondamentales de ces systèmes qui s'avèrent nécessaires dès
 +qu'on modélise un domaine informatique par un système de réécriture:
 +la confluence, la terminaison, les stratégies, l'unification, la
 +complétion, etc.
 +
 +Le cours introduit les notions de bases de la réécriture dans un cadre
 +du premier ordre, puis dans un cadre d'ordre supérieur. On montrera
 +aussi le lien entre ces deux mondes à l'aide de calculs avec
 +substitutions
 +explicites.
 +
 +==== Plan du cours ====
 +
 +   * Systèmes de réduction abstraits
 +   * Réécriture du premier ordre
 +    * Termes algébriques
 +    * Différentes notions de réduction
 +    * Problèmes équationnels
 +    * Unification
 +    * Paires critiques
 +    * Confluence
 +    * Terminaison
 +    * Modularité
 +    * Stratégies de réduction
 +   * Théorèmes fondamentaux du lambda calcul
 +    * Confluence
 +    * Stratégies de réduction
 +    * Résidus et déplacements parallèles
 +    * Standardisation
 +    * Développements finis
 +    * Typabilité et Curry-Howard
 +    * Normalisation
 +    * Separabilité
 +   * Systèmes d'ordre supérieur
 +    * Différents formalismes
 +    * Confluence
 +    * Terminaison
 +    * Substitutions explicites
 +    * Traduction de la réécriture d'ordre supérieur en réécriture du premier ordre
 +
 +==== Pré-requis ====
 +
 +   * Notions élémentaires de logique
 +   * Notions élémentaires de programmation fonctionnelle
 +
 +==== Bibliographie ====
 +
 +   * H. Barendregt, The Lambda Calculus: Its Syntax and Semantics. North Holland, 1984.
 +   * F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.
 +   * Term Rewriting Systems. Terese. M. Bezem and J-W. Klop and R. de Vrijer editors. Cambridge Tracts in Theoretical Computer Science (55), 2003.
 +   * G. Huet. Constructive Computation Theory. Notes de cours disponibles sur http://pauillac.inria.fr/~huet/bib.html .
 +
 +==== Équipe pédagogique ====
 +|G. Huet|DR|INRIA|Rocquencourt|
 +|D. Kesner|PU|Paris 7|PPS|
 +|T. Hardin|PU|Paris 6|LIP6|
 +
 +
 +==== Les années précédentes ====
 +
 +      * [[2009-2010-C-2-21|Année 2009-2010]]
 +** Année  [[2008-2009-C-2-21|2008-2009]]
 +
 +------
 +   * Set ALLOWTOPICCHANGE = %MAINWEB%.WebMastersGroup, %MAINWEB%.DeliaKesner, %MAINWEB%.GerardHuet
 +
  
 
Universités partenaires Université Paris-Diderot
Université Paris-Saclay
ENS Cachan École polytechnique Télécom ParisTech
ENS
Établissements associés Université Pierre-et-Marie-Curie CNRS INRIA CEA