Testing Concurrent Systems: An Interpretation of Intuitionistic Logic

Abstract. We present a natural confluence of higher-order hereditary Harrop formulas (HH formulas), Constraint Logic Programming (CLP, [JL87]), and Concurrent Constraint Programming (CCP, [Sar93]) as a fragment of (intuitionistic, higher-order) logic. This 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 syntax, and the power of constraints is needed to naturally abstract the underlying domain of computation. Underpinning the 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 deï¬...

• Type: Conference
• Year: 2005
• Where: FSTTCS
• Authors: Radha Jagadeesan, Gopalan Nadathur, Vijay A. Saraswat
• Keywords: Constraint Logic Programming, FSTTCS 2005, Hereditary Harrop Formulas, HH Formulas