Gopalan Nadathur, U Minnesota

Vijay Saraswat, IBM TJ Watson Research Center

June 25, 2005

*Submitted for publication.*

We present the natural confluence of higher-order hereditary Harrop
formulas (`HH`

formulas) as developed concretely in Lambda Prolog,
Constraint Logic Programming (`CLP`

), and Concurrent Constraint
Programming (`CCP`

) as a fragment of (intuitionistic, higher-order)
logic. The combination is motivated by the need for a simple
executable, logical presentation for static and dynamic semantics of
modern programming languages. The power of `HH`

formulas is needed
for higher-order abstract syntax, and the power of constraints is
needed to naturally abstract the underlying domain of computation.

Underpinning this combination is a sound and complete operational
interpretation of a two-sided sequent presentation of (a large
fragment of) intuitionistic logic in terms of *behavioral testing of
concurrent systems*. Formulas on the left hand side of a sequent style
presentation are viewed as a system of concurrent agents, and formulas
on the right hand side as *tests* against this evolving
system. The language permits recursive definitions of agents and
tests, allows tests to augment the system being tested and allows
agents to be contingent on the success of a test.

We present a condition on proofs, *operational derivability* (OD),
and show that the operational semantics generates only operationally
derivable proofs. We show that a sequent in this logic has a proof iff
it has an operationally derivable proof.

`G =>D`

(bottom of Page 7) has a typo. That paragraph
should be read as:
```
G => D. This interacts with Lambda by testing whether Lambda
passes G (using G => D as a resource if needed) and, if so, by
running D in parallel with Lambda. Thus we should require
Lambda, G => D ||- c iff for some Lambda': ((Lambda, G=>D),
c) -*-> ((Lambda', G=>D), c), and (i) Lambda' ||- c
or (ii) Lambda', G=>D ||- G and Lambda', D ||- c.
Notice that, in contrast to E, G functions as a deep guard in this
kind of agent formula. Further, the evolution of ((Lambda, G=>D),
c) may itself involve a recursive use of G=>D, but this time in
the context of establishing G' for a different G'=>D' in the
current configuration.
```

Correspondingly the formal rule for Deep Guard in Appendix C should be changed to:

```
Deep guard: Lambda, G => D ||- c iff for some Lambda': ((Lambda, G=>D),
c) -*-> ((Lambda', G=>D), c), and (i) Lambda' ||- c
or (ii) Lambda', G=>D ||- G and Lambda', D ||- c.
```