Since the introduction of linear logic in 1987, there have been various attempts to model asynchronous communications in process calculi using linear logic directly. There have been claims that linear logic should a good setting to make such specifications. To date, however, work in this area has progressed largely in two separate directions.
First: there is work showing that linear logic contains fragments that appear to encode asynchronous communications. See, for example, papers by Kobayashi & Yonezawa, by Miller, and by Cervesato & et.al.
Second: Various high-level asynchronous calculi have been designed either independently or partially inspired by logic and proof search. For example, there are is the asynchronous pi-calculus, spi-calculus (see Abadi & Gordon), and the chemical abstract machine and the join calculus (see Fournet & Gonthier).
The goal of this training project is to select some asynchronous formalisms designed outside the linear logic setting and see how well these can be encoded into linear logic. The quality of the encoding will be judged at two levels:
PhD thesis topics are possible based on work done for this stage. In particular, once connections are made at the level of communication primitives, one might next study recent additional expressiveness of process calculi (such as distribution and locality) and see to what extent these concepts can be addressed by logic. Several other directions are also possible.
The following bibliography is indicative of the kind of papers that will be part of this research effort. To find online copies, try searching using scholar.google.com.
A calculus for cryptographic protocols: The spi calculus, by Martín Abadi and Andrew D. Gordon. Information and Computation 1999, 148(1), pp. 1-70.
Distributed concurrent linear logic programming. by N. Kobayashi, T. Shimizu, and A. Yonezawa. Theoretical Computer Science, 227(1-2):185-220, 1999.
Asynchronous communication model based on linear logic. by Naoki Kobayashi and Akinori Yonezawa. Formal Aspects of Computing, 3:279-294, 1994.
The reflexive CHAM and the join-calculus, by Fournet and Gonthier, POPL 1996, 372--385.
A meta-notation for protocol analysis, by Cervesato, Durgin, Lincoln, Mitchell, and Scedrov. Proceedings of the 12th IEEE Computer Security Foundations Workshop --- CSFW'99, pages 55--69, Mordano, Italy, 28--30 June 1999.
Relating strands and multiset rewriting for security protocol analysis, by Cervesato, Durgin, Lincoln, Mitchell, and Scedrov. In P. Syverson, editor, 13th IEEE Computer Security Foundations Workshop --- CSFW'00, pages 35--51, Cambrige, UK, 3--5 July 2000.
Encryption as an abstract data-type: An extended abstract, by Dale Miller. FCS 2003: Foundations of Computer Security. Edited by Iliano Cervesato, pp. 3-14, June 2003. (DVI, PDF, PS). Slides used for talk: PDF.
Forum: A Multiple-Conclusion Specification Logic, by Dale Miller. Theoretical Computer Science 165(1): 201-232 (1996). (DVI, PDF, PostScript).