Faculté informatique et communications IC, Section d'informatique (Laboratoire de méthodes de programmation 1 LAMP1)

Foundations for SCALA : semantics and proof of virtual types

Cremet, Vincent ; Odersky, Martin (Dir.)

Thèse sciences Ecole polytechnique fédérale de Lausanne EPFL : 2006 ; no 3556.

Ajouter à la liste personnelle
    Summary
    SCALA is an attractive programming language because it is both very expressive and statically strongly typed. This marriage against nature comes at the price of a certain complexity in the language constructs and the static analysis. This complexity makes type safety unclear. The goal of this thesis is to initiate a rigorous and formal process of validation of the SCALA type system. The correctness of a type system can only be established in relation to a formal description of a program execution. The first contribution of this thesis is the definition of a formal semantics for SCALA, by translation in a minimal class-based calculus. SCALA offers two means for expressing type abstraction: type parameters and type members, also called virtual types. Virtual types seem more primitive since they allow to encode type parameters whereas the existence of a reverse encoding is not clear. The soundness of virtual types has been the object of a long debate in the community; they are now commonly believed to be safe, but at this time, there exists no formal argument that would confirm this belief. The second contribution of this thesis is to provide a formal proof of type safety for virtual types.
    Résumé
    SCALA est un langage de programmation attractif parce qu'il est à la fois expressif et fortement typé statiquement. Ce mariage contre nature vient au prix d'une certaine complexité dans les constructions du langage et dans l'analyse statique. Cette complexité rend la sûreté du typage incertaine. Le but de cette thèse est d'initier un processus de validation du système de typage de SCALA qui soit à la fois rigoureux et formel. La correction d'un système de typage ne peut être établie que par rapport à une description formelle de l'exécution d'un programme. La première contribution de cette thèse est la définition d'une sémantique formelle de SCALA, par traduction dans un calcul minimal basé sur les classes. SCALA donne deux moyens d'exprimer des abstractions de types : les paramètres de types et les membres de types, aussi appelés types virtuels. Les types virtuels paraissent plus primitifs vu qu'ils permettent d'encoder les paramètres de types alors que l'inverse n'est pas avéré. La correction des types virtuels a été l'objet d'un long débat dans la communauté, et il est désormais admis qu'ils sont sûrs. Cependant, à ce jour, aucun argument formel n'est venu confirmer cette croyance. La deuxième contribution de cette thèse est une preuve formelle de correction des types virtuels.