Title: Preemptive type checking

Abstract: 
In dynamically typed languages the type of any expression is determined through runtime computations. Consequently, a guarantee that a program will not raise any type errors during its execution cannot be computed precisely before its execution. We describe a new type checking mechanism that identifies potential type errors in advance through a flow-sensitive static analysis. It computes for every variable and program point an overapproximation of the variable's present (from the values that it has last been assigned) and future (with which it is used in the further program execution) types, respectively.  If the future types are not subsumed by the present types, the further program execution may raise a type error, and a narrowing assertion is inserted; if future types and present types are disjoint, it will raise a type error, and a type error assertion is inserted.  We prove that the assertions, as early as possible, preempt type errors earlier than in dynamic typing and also gradual and soft typing.  We further show that these assertions do not change the semantics of programs that do not raise type errors. We demonstrate the results of an innovative implementation for Python bytecode with a number of benchmarks and examples.