Testing concurrent systems: An interpretation of intuitionistic logic

Radha Jagadeesan, Gopalan Nadathur, Vijay Saraswat

Research output: Chapter in Book/Report/Conference proceedingConference contribution

21 Scopus citations

Abstract

We present a natural confluence of higher-order hereditary Harrop formulas (HH formulas), Constraint Logic Programming (CLP, [JL87]), and Concurrent Constraint Programming (COP, [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 abstract 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 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.

Original languageEnglish (US)
Title of host publicationFSTTCS 2005
Subtitle of host publicationFoundations of Software Technology and Theoretical Computer Science - 25th International Conference, Proceedings
Pages517-528
Number of pages12
DOIs
StatePublished - 2005
Event25th International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2005 - Hyderabad, India
Duration: Dec 15 2005Dec 18 2005

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3821 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other25th International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2005
Country/TerritoryIndia
CityHyderabad
Period12/15/0512/18/05

Fingerprint

Dive into the research topics of 'Testing concurrent systems: An interpretation of intuitionistic logic'. Together they form a unique fingerprint.

Cite this