View source for Seminar/2012-02-15

{{SeminarHeader
| id = 2012-02-15
| date = Mercredi 15 février 2012
| schedule = 14h-17h
| location = Salle Master
}}
{{Talk
| id = 2012-02-15
| abstract = «The effective exploitation of his powers of abstraction must be
regarded as one of the most vital activities of a competent
programmer.» disait Dijsktra.

En effet, pour aborder la complexité d'un problème, l'explicitation
des concepts utiles à sa formalisation et à sa résolution est bien
souvent une étape clé. Lorsque que l'on étend ce processus à une
classe de problèmes qui partagent les mêmes concepts, il est naturel
de se doter d'un langage le plus approprié possible pour manipuler ces
abstractions spécifiques à un domaine (en anglais, «Domain Specific
Language»).

Comment implémenter ces DSLs? Une première approche classique reflète
les constructions du DSL sous la forme d'un jeu de fonctions de
bibliothèque. L'avantage de cette approche est d'utiliser directement
son langage généraliste préféré, et sa chaîne de compilation
optimisée, de façon à générer du code machine à moindre frais. Par
contre, dans ce cadre, l'écriture de passe d'optimisations spécifiques
au DSL -- à moins d'utiliser des techniques pointues de
méta-programmation -- est a priori impossible.

Une seconde approche, opposée, consiste à écrire un compilateur pour
le DSL à partir de zéro. Toute liberté est alors donnée à
l'implémenteur d'intégrer à son compilateur des passes d'optimisation
spécifiques… mais au prix d'une réimplémentation de passes de
compilation déjà présentes, et certainement plus abouties, dans le
compilateur de son langage généraliste favori.

Dans cet exposé, je présenterai les travaux de Martin Odersky et
son équipe sur la virtualisation de DSLs à l'intérieur du langage de
programmation Scala. La virtualisation de langage utilise
intensivement le polymorphisme et la composition mixin de Scala ainsi
que des techniques de génération de code à l'exécution pour embarquer
des langages spécifiques dans Scala dont la compilation peut
réutiliser des modules du compilateur mais aussi étendre ces derniers
par des optimisations spécifiques au domaine.
| duration = 1h30
| orator = Yann Régis-Gianas
| resume = Yann Régis-Gianas est un ancien élève de l'EPITA, promo CSI 2003. À sa
sortie de l'école, il a poursuivi un troisième cycle en passant un DEA
à l'Université Paris Diderot et une thèse à l'INRIA Rocquencourt. Il
est aujourd'hui maître de conférence à Paris Diderot et travaille sur
le design des langages de programmation et de preuve.
| schedule = 14h
| slides = yrg-dsl-virtualization.pdf,matrixvirtualized.scala
| title = Des performances dans les nuages avec la virtualisation des langages
| urls = http://www.pps.jussieu.fr/~yrg/
}}{{Talk
| id = 2012-02-15
| abstract = Nous traitons du problème de la conception d'un compilateur où des
informations sur le coût à l'exécution du code objet sont retournées
en tant qu'annotations de coût sur le code source, et ce de façon
certifiée correcte. Pour cela, nous avons besoin d'une idée souple et
précise : (i) du sens donné aux annotations de coût, (ii) de la
méthode pour les prouver correctes et précises, et (iii) de la manière
d'en composer les preuves. Nous proposons ce que nous appelons une
approche par étiquetage pour répondre à ces trois questions. Dans un
premier temps, nous montrons son application sur un compilateur jouet.
L'étude formelle qui en découle suggère que l'approche par étiquetage
a de bonnes propriétés de compositionnalité et de passage à l'échelle.
Afin de s'en convaincre davantage, nous rapportons notre retour
d'expérience sur l'implémentation d'un compilateur prototype écrit en
ocaml pour un large sous-ensemble du langage C.
| duration = 1h30
| orator = Nicolas Ayache
| resume = Nicolas Ayache, ancien doctorant Université Paris-Sud / CEA-LIST, est
actuellement Post-doc au laboratoire PPS (Preuves, Programmes et
Systèmes) à l'université Paris Diderot.
| schedule = 15h30
| slides = ayache_EPITA.pdf
| title = Certification d'annotations de coût dans les compilateurs
| urls = 
}}