Inactive.
Set constraint types are a generalization of the standard notion of “type” to types which are sets of constraints about program behavior. Set constraints can capture more details about the potential values that can be in a variable than a traditional type system. For instance, in an object-oriented language such as Java, a variable declared as “Serializable” by the Java type system can be any object which conforms to the Serializable interface, but in practice that variable will only contain the concrete objects which the program in fact serializes. Knowing the precise classes the program is serializing at that point is useful both as a programming aid and as a tool to assist compilers in generating faster code. Recently we have developed and implemented a tool which statically checks whether Java downcasts are legal using a set-constraint-based mechanism.
Type constraint systems are a very expressive form of type which can be given to programs. They are so expressive that they can in fact fully record flow information about a program, namely this data value could flow to that operation.
The development of rich type constraint systems for object-oriented programming languages.
Our primary goal has been the extension of type constraint system to allow for greater expressivity and usefulness in typing more properties of programs.
Fine-grained type systems for flexible object-oriented languages.
Fine-grained program analysis for compilers and other static analysis consumers.
Tiejun Wang and Scott Smith, Precise Constraint-Based Type Inference for Java. ECOOP 2001. Full version.
Precise type information is invaluable for analysis and optimization of object-oriented programs. Some forms of polymorphism found in object-oriented languages pose significant difficulty for type inference, in particular data polymorphism. Agesen’s Cartesian Product Algorithm (CPA) can analyze programs with parametric polymorphism in a reasonably precise and efficient manner, but CPA loses precision for programs with data polymorphism. This paper presents a precise constraint-based type inference system for Java. It uses Data Polymorphic CPA, a constraint-based type inference algorithm which extends CPA with the ability to accurately and efficiently analyze data polymorphic programs. The system is implemented for the full Java language, and is used to statically verify the correctness of Java downcasts. Benchmark results are given which show the system performs very well: it is significantly more accurate and is nearly as efficient as CPA. The implementation itself contains a number of novel optimizations which proved necessary to achieve scalability.
Scott Smith and Tiejun Wang, Polyvariant Flow Analysis With Constrained Types. In Gert Smolka, editor, Proceedings of the 2000 European Symposium on Programming (ESOP’00), volume 1782 of Lecture Notes in Computer Science, pages 382–396. Springer Verlag, March 2000.
The basic idea behind improving the quality of a monovariant control flow analysis such as 0CFA is the concept of polyvariant analyses such as Agesen’s Cartesian Product Algorithm (CPA) and Shivers’ nCFA. In this paper we develop a novel framework for polyvariant flow analysis based on Aiken-Wimmers constrained type theory. We develop instantiations of our framework to formalize various polyvariant algorithms, including nCFA and CPA. With our CPA formalization, we show the call-graph based termination condition for CPA will not always guarantee termination. We then develop a novel termination condition and prove it indeed leads to a terminating algorithm. Additionally, we show how data polymorphism can be modeled in the framework, by defining a simple extension to CPA that incorporates data polymorphism.
V. Trifonov, S.Smith, Subtyping Constrained Types, Static Analysis Symposium (SAS) 1996, Lecture Notes in Computer Science 1145, pp. 349-365.
Constrained type systems are a natural generalization of Hindley/Milner type inference to languages with subtyping. This paper develops several subtyping relations on constrained types. We establish a full type abstraction property that equates an operational notion of subtyping with a semantic notion based on regular trees. The decidability of this notion of subtyping is open; we present a decidable approximation. Subtyping constrained types has application to functor signature matching.
J. Palsberg, S. Smith, Constrained Types and their Expressiveness, TOPLAS 18 (5), Sept 1996, pp. 519-527.
Kim B. Bruce, Luca Cardelli, Giuseppe Castagna, The Hopkins Objects Group, Gary T. Leavens, and Benjamin Pierce. On Binary Methods, Theory and Practice of Object Systems 1 (3), 1995, pp. 217-238. Department of Computer Science, Iowa State University, TR95-08, May 1995.
J. Eifrig, S. Smith, V. Trifonov, Sound Polymorphic Type Inference for Objects, OOPSLA 1995, pp. 169-384.
J. Eifrig, S. Smith, V. Trifonov, Type Inference for Recursively Constrained Types and its Application to OOP (longer version), Mathematical Foundations of Programming Semantics 1995 (Elsevier Electronic Notes in Theoretical Computer Science, volume 1).
J. Eifrig, S. Smith, V. Trifonov, A. Zwarico, Application of OOP Type Theory: State, Decidability, Integration, OOPSLA 1994, pp. 16-30.
J. Eifrig, S. Smith, V. Trifonov, A. Zwarico, An Interpretation of Typed OOP in a Language with State, Lisp and Symbolic Computation 8 (4), 1995, pp. 357-397.
J. Eifrig, S. Smith, V. Trifonov, A. Zwarico, A Simple Interpretation of OOP in a Language with State, Workshop on State in Programming Languages 1993, pp. 1-36.