Skip to Main content Skip to Navigation

A formalization of Static Analyses in System F

Abstract : 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).
Document type :
Complete list of metadatas

Cited literature [20 references]  Display  Hide  Download
Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 9:06:59 AM
Last modification on : Wednesday, November 20, 2019 - 3:14:32 AM


Files produced by the author(s)


  • HAL Id : hal-02101813, version 1



Frederic Prost. A formalization of Static Analyses in System F. [Research Report] LIp RR-1999-07, Laboratoire de l'informatique du parallélisme. 1999, 2+25p. ⟨hal-02101813⟩



Record views


Files downloads