Seminar/2009-03-25

Mercredi 25 mars 2009, 14h-15h30, Amphi 2

Que se cache-t-il derrière ce type ?

Documents

regis-gianas.pdf

Yann Régis-Gianas, laboratoire PPS (Univ. Paris Diderot), équipe πr² (INRIA)

Si une fonction φ promet de manipuler une valeur de type α sans l'observer, on peut utiliser son code sans risque pour toutes les affectations possibles de α : que la valeur soit entière (α = int) ou qu'elle soit un arbre (α = tree), la fonction se comportera toujours de façon identique. Cette propriété s'appelle le polymorphisme paramétrique, l'essence de la généricité.

Promettre de ne pas observer de trop près son argument est un fardeau parfois insupportable pour une fonction, pour des raisons algorithmiques (comment prendre une décision sans savoir ce que vaut mon argument ?), ou encore pour des raisons de performances de bas-niveau (si je sais que α = int, je peux utiliser une primitive dédiée de mon processeur). Même si le type d'une valeur est caché derrière un type plus abstrait α, on peut fournir des mécanismes pour « le redécouvrir » grâce à des tests dynamiques ou à des raisonnements purement statiques. La propriété qui permet de diriger son calcul par la forme des types est appelée le polymorphisme intentionnel.

Dans cet exposé, nous présenterons plusieurs versions du polymorphisme intentionnel offertes par différents systèmes de types et de preuves sûrs (c'est-à-dire garantissant que les programmes ne peuvent pas planter et sont corrects vis-à-vis de leur spécification).

Yann Régis-Gianas est maître de conférence de l'Université Paris Diderot. Ancien élève de l'EPITA et du LRDE (promo CSI 2003), il a poursuivi son cursus par un DEA SPL (précurseur de l'actuel MPRI) et par un doctorat au sein de l'équipe Gallium de l'INRIA. Il étudie le design des langages de programmation à typage statique garantissant l'absence d'erreurs dans les programmes.

http://www.pps.jussieu.fr/~yrg