Testing concurrent systems: An interpretation of intuitionistic logic

Radha Jagadeesan, De Paul University
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.

Erratum (07/28/05)

The informal definition of the testing interpretation for the agent 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.


Powerpoint slides (Revision of FSTTCS presentation)

Back to Main page