A formalization of static analyses in system F

Abstract

In this paper, we propose a common theoretical framework for type based static analyses. The aim is the study of relationships between typing and program analysis. We present a variant of Girard’s System F called (formula presented). We prove standard properties of Fn. We show 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 expressivness (often only simply typed calculi are considered) and power (more information can be inferred). (formula presented) features polymorphism as well as subtyping at the level of universe extending previous author work where only universe polymorphism (on a simply typed calculus) was considered.