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 :
Reports
Complete list of metadatas

Cited literature [20 references]  Display  Hide  Download

https://hal-lara.archives-ouvertes.fr/hal-02101813
Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 9:06:59 AM
Last modification on : Wednesday, May 22, 2019 - 1:32:16 AM

File

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

Identifiers

  • HAL Id : hal-02101813, version 1

Collections

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⟩

Share

Metrics

Record views

14

Files downloads

34