Journal Nécrologie : Robin Milner.

Posté par  (site web personnel) .
Étiquettes :
34
23
mar.
2010
Il y a quelques jours, nous apprenions sur la mailing-list "TYPES" le décès de Robin Milner [1], qui nous a quitté le 20 mars 2010.


Il est probable que beaucoup d'entre vous ne sachent pas qui Robin Milner était, alors je me permets de faire une rapide biographie :
Né en Angleterre en 1934, il fait une carrière académique qui l'envoit notamment à Stanford, Edinburgh (où il co-fonde le Laboratory for Foundations of Computer Science [2]) et à Cambridge où il sera chef du département d'informatique.


En quoi Milner nous intéresse-t-il ?
Eh bien d'une part, Milner a créé un des premiers assistants de preuve et pour ce faire, a développé le langage ML. Le langage ML, dont des descendants actuels connus sont OCaml et Haskell, fut le premier langage avec inférence de types polymorphes (ce qui permet donc d'écrire un programme valide comme 'let f x = x in (f 3, f "bar")') et système d'exceptions bien typé ; on parle d'ailleurs toujours de l'algorithme d'inférence Hindley-Milner qui est à la base de bien d'autres très utilisés de nos jours. Difficile aujourd'hui de se passer d'un système de types (dynamique ou statique) dans un langage de programmation, et de faire confiance à du code dans des application critiques qui n'a pas été prouvé formellement (même s'il reste du travail à faire).
D'autre part, Robin Milner est un des pionniers de l'étude des systèmes concurrents, avec sa recherche sur CCS et le π-calcul [3] (et dernièrement les bigraphes [4]). Il a proposé un formalisme simple pour étudier le parallélisme et ses problèmes, comme les f{a,u}meux « race conditions » ou situations de compétition, et sur lequel encore beaucoup de recherche se fonde.

Son influence sur l'informatique moderne est indéniable, et il obtint en 1991 le fameux Turing Award [5] pour ses travaux, pour ne citer qu'une seule des distinctions qui lui furent accordées.


J'ai eu la chance de suivre trois mois de cours (presque particuliers) avec lui sur les bigraphes en 2007 et je suis touché par sa disparition.

En espérant que ce journal ne vous dépayse pas trop [6], je vous saurai gré d'avoir une pensée magnanime pour ce chic type.


[1] : http://lists.seas.upenn.edu/pipermail/types-list/2010/001478(...)
[2] : http://www.lfcs.inf.ed.ac.uk/
[3] : http://fr.wikipedia.org/wiki/Pi-calcul
[4] : http://www.cl.cam.ac.uk/~rm135/uam-theme.html
[5] : http://awards.acm.org/citation.cfm?id=1569367&srt=alpha&alph(...)
[6] : https://linuxfr.org//~OlivierL/15140.html

  • # Lapin compris

    Posté par  . Évalué à 9.

    Qu'entends-tu par décès ? De quoi s'agit-il ?

  • # Un des « grands anciens »

    Posté par  . Évalué à 4.

    Robin Milner est un de ces pionniers dont les travaux ont forcément affecté, directement ou non, à peu près tout le monde. Il m'a, de plus, laissé l'impression d'un gentil monsieur très intéressant à écouter, même si en ce qui me concerne je ne l'ai entendu que pendant une de ses journées de visite en France, pas comme ces veinards qui en ont eu pour trois mois :-).

    Pour ma part, c'est surtout le pi-calcul qui m'a marqué, sans doute parce qu'on m'a présenté la synthèse de types sans l'aspect historique. J'ai été très impressionné de voir que l'on pouvait définir un formalisme aussi simple et propre, qui est aux systèmes concurrents ce que le lambda-calcul est aux systèmes séquentiels, dans lequel la notion même de communication devient fondamentale.

    • [^] # Re: Un des « grands anciens »

      Posté par  . Évalué à 3.

      [...] qui est aux systèmes concurrents ce que le lambda-calcul est aux systèmes séquentiels,

      En même temps le lambda-calcul a une légitimité que le pi-calcul n'a pas, au sens où tout le monde s'accorde à dire qu'il est le socle de base du calcul séquentiel, alors que les gens s'entre-déchirent encore pour savoir quel est le bon formalisme ultime pour la concurrence : s'agit-il de CCS, CSP, d'une des 42 variantes du pi-calcul, des ambiants, d'un formalisme basé sur les automates, des réseaux de Petri, de la logique linéaire différentielle... ?! À titre d'exemple, Milner travaillait dans ses dernières années sur les « bigraphs », qui sont encore un autre formalisme, très graphique cette fois-ci et assez différent de ses essais précédents (CCS et le pi-calcul).

      Les grandes idées ont probablement émergé mais il semble que le domaine ne soit pas encore assez mûr pour offrir une vision unifiée et propre de ce qu'est la concurrence. Les papiers « Yet Another Process Calculus » ont encore de beaux jours devant eux à CONCUR et ailleurs.

Suivre le flux des commentaires

Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.