Previous Projects
This page summarizes activity in past projects, including Specification Diagrams, Foundations of Actor Computation, Foundations of Operational Semantics, Hardware Verification, and Constructive Type Theory.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.
- A rigorous reworking of the Actor model of computation
- Operational semantics of executions given.
- Only fair executions considered, for unfair executions never arise in practice.
- Observational equivalence and methods for proving observational equivalence in the presence of fairness are defined.
- Explicit, dynamic modeling of external agents and their interactions.
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.
- The translation is defined by a set of rewrite rules, broken into five phases.
- A new notion of "translational equivalence" is defined to state how a translation preserves meaning when the language itself is changing.
- Only fair executions considered, for gates are inherently fair. This is some of the first work in circuit theory to consider fairness.
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, 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.).