9400907 Miller Computational aspects of proofs systems may be generally divided into two kinds. In what may be broadly called functional programming, computation is seen as term reduction corresponding to proof reduction (i.e., to the process of cut elimination). On the other hand, in what may be broadly called logic programming, computation is expressed by goal directed, cut free proof search in certain formal theories. This characterization of the logic programming paradigm is based on Miller's and Scedrov's earlier joint work. The proposed research is aimed at understanding the proof systems arising from linear logic, their computational and descriptive powers, and their semantics by means of interactive protocols. Game-theoretic notions, such as interactive protocols, should contribute to the understanding of "fine structure" of both semantics and computational expressiveness of linear logic. In the logic programming setting, such proof systems provide primitives for handling contexts and communications among resources. A proposed specification language based on this style of proof system can be used to declaratively and naturally specify such aspects of computation as side-effects, communications, and continuations. ***
