# 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).
Keywords :
Document type :
Reports
Domain :

Cited literature [20 references]

https://hal-lara.archives-ouvertes.fr/hal-02101813
Contributor : Colette Orange Connect in order to contact the contributor
Submitted on : Wednesday, April 17, 2019 - 9:06:59 AM
Last modification on : Saturday, September 11, 2021 - 3:19:19 AM

### File

RR1999-07.pdf
Files produced by the author(s)

### Identifiers

• HAL Id : hal-02101813, version 1

### Citation

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⟩

### Metrics

Les métriques sont temporairement indisponibles