Abstract
We analyze in game-semantical terms the finitary fragment of the linear π-calculus. This calculus was introduced by Yoshida, Honda, and Berger [NYB01], and then refined by Honda and Laurent [LH06].
The features of this calculus - asynchrony and locality in particular - have a precise correspondence in Game Semantics. Building on work by Varacca and Yoshida [VY06], we interpret π-processes in linear strategies, that is the strategies introduced by Girard within the setting of Ludics [Gir01]. We prove that the model is fully complete and fully abstract w.r.t. the calculus.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Curien, P.-L., Faggian, C.: L-nets, strategies and proof-nets. In: Ong, L. (ed.) CSL 2005. LNCS, vol. 3634, Springer, Heidelberg (2005)
Faggian, C.: Linear logic games: Sequential and parallel. draft (2005)
Faggian, C., Piccolo, M.: A graph abstract machine describing event structure composition (short paper). In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, Springer, Heidelberg (2006)
Faggian, C., Piccolo, M.: Event structures and linear strategies (submitted)
Girard, J.-Y.: Locus solum. Mathematical Structures in Computer Science 11, 301–506 (2001)
Hyland, M., Ong, L.: On full abstraction for PCF. Information and Computation (2000)
Vasconcelos, V., Honda, K., Yoshida, N.: Secure information flow as typed process behaviour. In: Smolka, G. (ed.) ESOP 2000 and ETAPS 2000. LNCS, vol. 1782, Springer, Heidelberg (Extended abstract) (2000)
Laurent, O., Honda, K.: An exact correspondence between a typed pi-calculus and polarised proof-nets. draft (2006)
Honda, K., Yoshida, N., Berger, M.: Sequentiality and the pi-calculus. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol. 2044, Springer, Heidelberg (Extended abstract) (2001)
Honda, K., Yoshida, N., Berger, M.: Strong normalisation in the pi-calculus. Journal of Information and Computation, full version ( 2003)
Sangiorgi, D., Walker, D.: The π-calculus: a Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)
Varacca, D., Yoshida, N.: Typed event structures and the pi-calculus. In: MFPS (2006)
Yoshida, N., Honda, K.: Noninterference through flow analysis. Journal of Functional Programming, revised (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Faggian, C., Piccolo, M. (2007). Ludics is a Model for the Finitary Linear Pi-Calculus. In: Della Rocca, S.R. (eds) Typed Lambda Calculi and Applications. TLCA 2007. Lecture Notes in Computer Science, vol 4583. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73228-0_12
Download citation
DOI: https://doi.org/10.1007/978-3-540-73228-0_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73227-3
Online ISBN: 978-3-540-73228-0
eBook Packages: Computer ScienceComputer Science (R0)