-----------------------------------------------------------------------------
An Operational Semantics Framework Supporting the Incremental
Construction of Derivation Trees
-----------------------------------------------------------------------------

I will describe the current state of the design and implementation of
Dops, a framework for Deterministic OPerational Semantics that will
support the incremental construction of derivation trees, starting
from term/input pairs.  This process of derivation tree expansion may
terminate with either a complete derivation tree, explaining why a
term/input pair evaluates to a particular output, or with a blocked
incomplete derivation tree, explaining why a term/input pair fails to
evaluate to an output; or the process may go on forever, yielding, in
the limit, an infinite incomplete derivation tree, explaining why a
term/input pair fails to evaluate to an output.

The Dops metalanguage is a typed lambda calculus in which all
expressions converge.  Semantic rules are specified by lambda terms
involving resumptions, which are used by a rule to consume the outputs
of sub-evaluations and then resume the rule's work.  A rule's type
describes the number and kinds of sub-evaluations that the rule can
initiate, and indicates whether the rule can block.  The semantics of
Dops is defined in an object language-independent manner as a
small-step semantics on concrete derivation trees: trees involving
resumptions.  These concrete derivation trees can then be abstracted
into ordinary derivation trees by forgetting the resumptions.

An preliminary paper on Dops can be found at

  http://www.cis.ksu.edu/~allen/papers.html