Inactive.
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.
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.