Previous Projects

This page summarizes activity in past projects, including Type Constraints, Specification Diagrams, Foundations of Actor Computation, Foundations of Operational Semantics, Hardware Verification, and Constructive Type Theory.

Type Constraints

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.

Goal: 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.

Uses:

Publications

Tiejun Wang and Scott Smith, Precise Constraint-Based Type Inference for Java. ECOOP 2001. Full version submitted to TOPLAS.
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.

Try Out the Inference Algorithm Here!


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.

Specification Diagrams for Distributed Systems

Specification diagrams are a graphical notation for the specification of distributed systems. The primary design goal is to make a form of notation for defining message-passing behavior that is very expressive, intuitively understandable, and that has a fully formal underlying semantics.

Specification diagrams are two-dimensional graphical structures. Many specification languages that have achieved widespread usage have a graphical foundation: engineers can understand and communicate more effectively by graphical means. Popular graphical specification languages include Universal Modelling Language (UML) and its predecessors, and StateCharts. Specification diagrams aim to be a language with similar intuitive advantage but significantly greater expressivity and formal underpinnings.

Specification diagrams are highly suited to protocol specification because they give a formal specification of the protocol that is also readable by implementers. We have specified various security protocols, including the Needham-Schroeder protocol and TLS.

Publications

Christian Skalka and Scott Smith, Verifying Security Protocols with Specification Diagrams, Technical Report, Johns Hopkins Unversity, 2002.

Scott Smith and Carolyn Talcott. Specification Diagrams for Actor Systems. Higher-order and Symbolic Computation (HOSC) 15, December 2002.

Scott Smith and Carolyn Talcott, Modular Reasoning for Actor Specification Diagrams. Formal Methods in Object-Oriented Distributed Systems, Florence, 1999. Kluwer Academic Publishers, to appear. The slides from the FMOODS talk.

Scott Smith, Specification Diagrams for Actor Systems. Higher Order Operational Techniques in Semantics II, Electronic Notes in Theoretical Computer Science, 1998.

Foundations of Actor Computation

The goal of this project is the development of rigorous semantic foundations for actor computation.

Here are a few features of the models we developed.

Publications

G. Agha, I. Mason, S. Smith, C. Talcott, A Foundation for Actor Computation. Journal of Functional Programming, volume 7, pages 1--72, 1997.

G. Agha, I. Mason, S. Smith, C. Talcott, Towards a Theory of Actor Computation. Third International Conference on Concurrency Theory (CONCUR), Lecture Notes in Computer Science 630, 1992.

Foundations of Operational Semantics

This line of research addresses foundational issues in operational semantics. The main thrust has been to show how denotational concepts such as pre-ordering on elements, directed set, least fixed-point, fixed point induction, finite/compact/algebraic elements, and ideal models of types can be "ported" to a purely operational semantic development. The goal of this research is to give full and faithful semantics to languages for which denotational semantics falls short.

Publications

I. Mason, S. Smith, C. Talcott, From Operational Semantics to Domain Theory, Information and Computation volume 128, pages 26--47, 1996.
This paper presents the operational theory for a pure functional language.

S. Smith, From Operational to Denotational Semantics. Conference on Mathematical Foundations of Programming Language Semantics, Lecture Notes in Computer Science 598, Springer-Verlag, 1992. (downloadable version is an extended version, but this paper is generally subsumed by the previous)

S. Smith, The Coverage of Operational Semantics . In Higher Order Techniques in Operational Semantics, A. Gordon and A. Pitts, editors, Cambridge University Press.
This paper studies how more complex languages may be fully and faithfully embedded in simpler ones. By such embeddings, some results which hold for purely functional languages can be lifted to languages with state and objects. A conjecture is given on how to characterize the finite or compact elements for a language with state; the problem remains open however.

F. Honsell, I. Mason, S. Smith, C. Talcott, A Variable Typed Logic of Effects. Information and Computation volume 119, pages 55-90, 1995. This paper develops a modal logic for a programming language with state.

Hardware Verification

In collaboration with Amy Zwarico we defined a formal language for specifying asynchronous digital circuits that is based on Hoare's CSP, and verified a translation of these circuit specifications to hardware devices (collections of gates). The translation was proven correct by defining a formal operational notion of equivalence, and incrementally translating the specification to the circuit in small steps that preserve equivalence. Numerous informal arguments of correctness of similar synthesis methods exist, but this work is the first complete, rigorous proof of correctness of such a method. Some other features of this project include the following.

Publications

S. Smith, A. Zwarico, Correct Compilation of Specifications to Deterministic Asynchronous Circuits. Formal Methods in System Design volume 7, 1995.

S. Smith, A. Zwarico, Correct Compilation of Specifications to Deterministic Asynchronous Circuits. Correct Hardware Design Methodologies, Arles, France, May 1993, Lecture Notes in Computer Science, volume 683.

Constructive Type Theory

The main contributions were in developing type systems that allow both partial and total functions to be typed in a single type theory.

Publications

S. Smith, Hybrid Partial-Total Type Theory. International Journal of Foundations of Computer Science volume 6, 235-263, 1995.
This paper is a simplified version of the results in my PhD thesis.

S. Smith, Reflective Semantics of Constructive Type Theory. Constructivity in Computer Science, Springer-Verlag LNCS 613, 1992.

S. Smith, Extracting Recursive Programs in Type Theory. AMAST 1991, Springer-Verlag Workshops in Computing Series.

S. Smith, Partial Objects in Type Theory (PhD Thesis)

Computational foundations of basic recursive function theory. Theoretical Computer Science, December 1993 (with Robert Constable).

Implementing Mathematics with the Nuprl Proof Development System. Englewood Cliffs: Prentice Hall, 1986 (with Robert Constable, et. al.).