A formalization of Static Analyses in System F
Résumé
We propose a variant of Girard's System F. The aim of this new system is to provide a common framework for various type based analyses. We modify $F$ by the introduction of two different universes from which types may be built. Following C. Paulin, those two universes may be seen as $Prop$ and $Spec$. The originality of our system lies on two points: 1) We define an inclusion relation between the two universes, from which we derive a subtyping relation on types. 2) We introduce a notion of {\em universe variable}, and develop a polymorphism \`a la ML on universes. We show that this system has the standard properties (conflence, SN, etc.) and how it can be used to formalize various program analyses like binding time and dead code. We relate our work to previous analyses in terms of expressiveness (often only simply typed calculi are considered) and power (more information can be inferred).
Dans ce papier,nous proposons un cadre théorique générique pour l'analyse statique de programmes fonctionnels. Le but poursuivi est l'étude des relations entre typage et analyse statique de programmes. Nous présentons une variante du système $F$ de Girard. Nous montrons que ce système satisfait les propriétés standards et utilisons ensuite ce système pour formaliser différentes analyses statiques de la littérature, et même de les dépasser à la fois en expressivité (souvent ne sont considérés que des calculs simplements typés) et en puissance (plus d'informations peuvent être déterminées sur un programme donné).
Origine : Fichiers produits par l'(les) auteur(s)
Loading...