Abstract
We use linProc (i.e. a typed process calculus based on the calculus of solos) in order to express computational processes generated by SlPCF−, namely a simple programming language conceived in order to program only linear functions. We define a faithful translation of SlPCF− on linProc which enables us to process redexes of SlPCF− in a parallel way. Afterward, we prove that a suitable observational equivalence between processes is correct w.r.t the operational semantics of SlPCF−, via our interpretation.
Paper partially supported by MIUR-Cofin’07 CONCERTO Project.
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
Abelson, H., Sussman, G.J., Sussman, J.: Structure and Interpretation of Computer Programs. MIT Press, Cambridge (1985), http://mitpress.mit.edu/sicp/full-text/book/book.html
Abramsky, S., Malacaria, P., Jagadeesan, R.: Full abstraction for PCF. Information and Computation 163(2), 409–470 (2000)
Beffara, E.: An algebraic process calculus. In: Proceedings of LICS 2008 (to appear, 2008)
Berger, M., Honda, K., Yoshida, N.: Sequentiality and the pi-calculus. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol. 2044, pp. 29–45. Springer, Heidelberg (2001)
Berry, G., Curien, P.-L., Lévy, J.-J.: Full abstraction for sequential languages: the state of the art. In: Nivat, M., Reynolds, J. (eds.) Algebraic Semantics, pp. 89–132. Cambridge University Press, Cambridge (1985)
Boreale, M., Sangiorgi, D.: A fully abstract semantics for causality in the π-calculus. Acta Informatica 35(5), 353–400 (1998)
Degano, P., Priami, C.: Causality for mobile processes. In: Fülöp, Z., Gécseg, F. (eds.) ICALP 1995. LNCS, vol. 944, pp. 660–671. Springer, Heidelberg (1995)
Hoare, C.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)
Honda, K., Yoshida, N.: On reduction-based process semantics. Theoretical Computer Science 151(2), 437–486 (1995)
Hyland, J.M.E., Ong, L.C.-H.: Pi-calculus, dialogue games and PCF. In: Proceedings of FPCA 1995, pp. 96–107. ACM Press, New York (1995)
Hyland, J.M.E., Ong, L.C.-H.: On full abstraction for PCF: I, II, and III. Information and Computation 163(2), 285–408 (2000)
Kobayashi, N., Pierce, B.C., Turner, D.N.: Linear types and the Pi-Calculus. In: 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL, pp. 358–371. ACM Press, New York (1996)
Kobayashi, N., Pierce, B.C., Turner, D.N.: Linearity and the Pi-Calculus. ACM Transactions on Computational Logic 21(5), 914–947 (1999)
Laneve, C., Victor, B.: Solos in concert. Mathematical Structures in Computer Science 13(5), 657–683 (2003)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1889)
Milner, R.: Functions as processes. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 167–180. Springer, Heidelberg (1990)
Milner, R.: Functions as processes. Mathematical Structures in Computer Science 2(2), 119–141 (1992)
Milner, R.: The polyadic π-calculus: A tutorial. In: Bauer, F.L., Brauer, W., Schwichtenberg, H. (eds.) Logic and Algebra of Specification, Proceedings of International NATO Summer School, Marktoberdorf, Germany, 1991, vol. 94. Springer, Heidelberg (1993)
Paolini, L.: A stable programming language. Information and Computation 204(3), 339–375 (2006)
Paolini, L., Piccolo, M.: Semantically linear programming languages. In: 10th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, Valencia, Spain, pp. 97–107. ACM, New York (2008)
Parrow, J., Victor, B.: The fusion calculus: Expressiveness and symmetry in mobile processes. In: Thirteenth Annual Symposium on Logic in Computer Science (LICS), Indiana, pp. 176–185. IEEE Computer Society Press, Computer Society Press, Los Alamitos (1998)
Plotkin, G.D.: Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science 1, 125–159 (1975)
Plotkin, G.D.: LCF considerd as a programming language. Theoretical Computer Science 5, 225–255 (1977)
Ronchi Della Rocca, S., Paolini, L.: The Parametric λ-Calculus: a Metamodel for Computation. In: Texts in Theoretical Computer Science. An EATCS Series, Springer, Berlin (2004)
Sangiorgi, D.: An investigation into functions as processes. In: Brookes, S.D., Main, M.G., Melton, A., Mislove, M.W., Schmidt, D.A. (eds.) MFPS 1993. LNCS, vol. 802, pp. 143–159. Springer, Heidelberg (1994)
Sangiorgi, D.: Internal mobility and agent-passing calculi. In: Fülöp, Z., Gecseg, F. (eds.) ICALP 1995. LNCS, vol. 944, pp. 672–683. Springer, Heidelberg (1995)
Sangiorgi, D., Walker, D.: The π-calculus: a theory of mobile processes. Cambridge University Press, Cambridge (2001)
Yoshida, N., Berger, M., Honda, K.: Strong normalisation in the PI-calculus. Information and Computation 191(2), 145–202 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Paolini, L., Piccolo, M. (2009). A Process-Model for Linear Programs. In: Berardi, S., Damiani, F., de’Liguoro, U. (eds) Types for Proofs and Programs. TYPES 2008. Lecture Notes in Computer Science, vol 5497. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02444-3_18
Download citation
DOI: https://doi.org/10.1007/978-3-642-02444-3_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02443-6
Online ISBN: 978-3-642-02444-3
eBook Packages: Computer ScienceComputer Science (R0)