Scientific Report

1 Scientific Activity Static analysis allows to formally prove properties of programs without having to execute them. Various properties can be proved using different techniques, e.g., type systems guarantee check well-formedness of programs or their termination, and bisimulations can be use to compare the behaviors of programs. During my fellowship, I studied such techniques for the λ-calculus extended with control operators. Such operators allow programs to manipulate their execution contexts, and can be used, e.g., to implement exceptions, backtracking algorithms, etc. Type systems. The first part of my fellowship was dedicated to the definition of an expansion mechanism for universal quantifiers. Expansion is an operation on typings (i.e., pairs of typing environments and result types) defined originally in type systems for the λ-calculus with intersection types in order to obtain principal (i.e., most informative, strongest) typings. In a type inference scenario, expansion allows postponing choices for whether and how to use non-syntax-driven typing rules (e.g., intersection introduction) until enough information has been gathered to make the right decision. With J. B. Wells, we have extended expansion to a system with ∀-quantifiers (System F). Our system turns type inference into a constraint solving problem; this could be helpful to design a modular type inference algorithm for System F types in the future. Thi