Journal article
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 second-order 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 concurrent threads 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, has a regular-language representation and thus the restricted observational equivalence is decidable.
- Publication status:
- Published
- Peer review status:
- Peer reviewed
Actions
Access Document
- Files:
-
-
(Preview, Version of record, pdf, 361.4KB, Terms of use)
-
- Publisher copy:
- 10.1016/j.tcs.2005.10.032
Authors
- Publisher:
- Elsevier
- Journal:
- Theoretical Computer Science More from this journal
- Volume:
- 350
- Issue:
- 2-3
- Pages:
- 234–251
- Publication date:
- 2006-02-01
- Edition:
- Publisher's version
- DOI:
- ISSN:
-
0304-3975
- Language:
-
English
- Keywords:
- Subjects:
- UUID:
-
uuid:c9fcbd8b-2adc-43c6-951d-ed6a6efc76e4
- Local pid:
-
ora:10762
- Deposit date:
-
2015-03-30
- ARK identifier:
Terms of use
- Copyright holder:
- Elsevier BV
- Copyright date:
- 2005
- Notes:
- Copyright 2005 Elsevier B.V. All rights reserved. Re-use of this article is permitted in accordance with the Terms and Conditions set out at http://www.elsevier.com/open-access/userlicense/1.0/
- Licence:
- Other
If you are the owner of this record, you can report an update to it here: Report update to this record