Syntactic Control of Concurrency

Abstract. We consider a finitary procedural programming language (finite data-types, no recursion) extended with parallel composition and binary semaphores. Having first shown that may-equivalence of secondorder open terms is undecidable we set out to find a framework in which decidability can be regained with minimum loss of expressivity. To that end we define an annotated type system that controls the number of conthreads created by terms and give a fully abstract game semantics for the notion of equivalence induced by typable terms and contexts. Finally, we show that the semantics of all typable terms, at any order and in the presence of iteration, admits a regular-language representation and thus the restricted observational equivalence is decidable.

• Type: Conference
• Year: 2004
• Where: ICALP
• Authors: Dan R. Ghica, Andrzej S. Murawski, C.-H. Luke Ong
• Keywords: ICALP 2004, Secondorder Open Terms, Theoretical Computer Science, Typable Terms, finitary Procedural Programming