Towards a type-based abstract semantics for Python

Python is a high-level programming language that is strongly, but dynamically typed. In this paper, we propose a type inference framework to compute specifications for Python functions in isolation. To achieve this, we aim to use an abstract-interpretation-based data flow analysis to infer variable types on a subset of Python programs that use built-in types, operators and functions. To evaluate the expressions found in every program point, specifications for the encountered operations and functions are required. We propose a method for extracting these specifications from the Typeshed project, which contains a set of annotations for built-in and popular third-party libraries. These specifications will be used then to extend the proposed type inference to large Python programs. • Static analysis is used to infer types of variables for a subset of Python programs. • The type inference is achieved by combining dataflow analysis, abstract interpretation, and a constraint solver. • Annotations can be translated to a more formal model, that can be used for variable type inference for larger programs.