Tom Hirschowitz http://perso.ens-lyon.fr/tom.hirschowitz Titre: Sémantique modulaire des langages de programmation Traditionnellement, la compilation des langages de programmation ne se prouve pas formellement. Pour certains aspects basiques de la compilation, ça ne fait pas trop peur et la preuve de correction manquante peut être vue comme une formalité. Cependant, d'autres aspects sont plus difficiles. Par exemple, on peut citer les constructions de haut niveau, comme les objets, les fonctions d'ordre supérieur, ou bien la programmation multi-niveaux. Une autre classe d'exemples est celle des optimisations poussées, faites par la partie back-end des compilateurs. Des travaux récents commencent à attaquer la question sérieusement [Chen et al., 2003; Leroy, 2006]. Notre expérience en la matière concerne la compilation efficace du let rec dans les langages fonctionnels en appel par valeur [Hirscho et al.], ainsi que des tentatives préliminaires de compilation d'un langage concurrent et distribué avec passivation de composants. Nous avons rencontré des difficultés croissantes, du cas purement fonctionnel étudié par Plotkin [1975] au cas concurrent et distribué, en passant par le cas du let rec, séquentiel mais comportant des traits impératifs. * D'une part, le traitement des réductions administratives s'est révélé de plus en plus crucial, jusqu'à dépasser nos compétences dans le dernier cas. Le terme de réduction administrative, employé à l'origine par Plotkin [1975], est pour l'instant informel et générique. En gros, il fait référence aux cas où le code compilé ne correspond au code source que modulo des ajustements inessentiels. Dans le cas concurrent et distribué, ces ajustements rendent la preuve de correction de la compilation techniquement inconfortable et combinatoirement ingérable. * D'autre part, la notion même d'équivalence entre le programme source et sa version compilée devient problématique. Dans le cas séquentiel, on demande généralement une simulation du code source par le code compilé, préservant la non-terminaison. Dans le cas concurrent et distribué, le caractère distribué de la passivation de composants que nous proposons ne permet pas une correspondance aussi précise. Nous avons eu recours à la notion de simulation couplée [Parrow et Sjodin, 1992], qui laisse plus de place aux ajustements entre code source et code compilé. Le choix de la notion d'équivalence semble être uniquement dicté par la technique: que faut-il demander pour que ça marche. Bien sûr, il y a des intuitions, mais rien de générique. Par exemple, en quoi devrions-nous être satisfaits par une simulation couplée entre code source et code compilé? Autrement dit: qu'est-ce qu'une notion d'observation et comment formaliser le fait que la compilation préserve l'observation? Ces deux difficultés sont liées: plus on relâche la correspondance entre code source et code compilé, plus il y a de réductions administratives et inversement, c'est bien parce qu'il est impossible de compiler efficacement certaines constructions qu'on est forcé de raffiner cette même correspondance. A la base du sujet de thèse proposé se trouve la constatation que la preuve de correction de sur le let rec [Hirscho et al.] procède par un découpage des programmes, douloureux techniquement mais indispensable, et surtout garde trace de ce découpage à la traduction et à l'exécution. En conséquence, le sujet proposé consiste en premier lieu à rendre plus locale la spécification des langages de programmation, ainsi, à terme, que leur compilation. En d'autres termes, il s'agit d'élaborer des méthodes systématiques pour effectuer le découpage évoqué et le prolonger, d'abord au cas par cas, à la compilation et à l'exécution. Techniquement, pour cette partie, des pistes semblent mener à la sémantique double catégorique de la logique linéaire [Mellies, 2002]. Si cette phase aboutit suffisamment rapidement, le thésard pourra se pencher sur la question de la notion d'observation et de sa préservation par compilation. Bibliographie * S. Abramsky and S. J. Vickers. Quantales, Observational Logic and Process Semantics. Mathematical Structures in Computer Science, Vol. 3, pp. 161-227, 1993. * Juan Chen, Dinghao Wu, Andrew W. Appel, and Hai Fang. A Provably Sound TAL for Back-end Optimization. PLDI 2003: ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 208-219, June 2003. * Tom Hirschowitz, Xavier Leroy, and J. B. Wells. Compilation of extended recursion in call-by-value functional languages. Under revision for publication in Higher-Order and Symbolic Computation. * Xavier Leroy. Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In 33rd symposium Principles of Programming Languages, pages 42-54. ACM Press, 2006. * Paul-André Melliès. Double categories: a modular model of multiplicative linear logic Mathematical Structures in Computer Science, vol. 12, pp 449-479, 2002. * J. Parrow and P. Sjodin. Multiway synchronization verified with coupled simulation. In Proceedings CONCUR 92, LNCS 630. Springer, 1992. * Gordon Plotkin. Call-by-Name, Call-by Value and the Lambda Calculus. Theoretical Computer Science, Vol. 1, pp. 125-159. Elsevier, 1975.