A Calculus for Constraint-Based Flow Typing
Author(s). David J. Pearce.
Venue. In Workshop on Formal Techniques for Java-like Languages (FTFJP), pages Article 7, 2013. ©ACM Press
Abstract: Flow typing offers an alternative to traditional Hindley-Milner type inference. A key distinction is that variables may have different types at different program points. Flow typing systems are typically formalised in the style of a dataflow analysis. In the presence of loops, this requires a fix-point computation over typing environments. Unfortunately, for some flow typing problems, the standard iterative fix-point computation may not terminate. We formalise such a problem we encountered in developing the Whiley programming language, and present a novel constraint-based solution which is guaranteed to terminate. This provides a foundation for others when developing such flow typing systems.