Abstract
We introduce a second-order polymorphic π-calculus based on duality principles. The calculus and its behavioural theories cleanly capture some of the core elements of significant technical development on polymorphic calculi in the past. This allows precise embedding of generic sequential functions as well as seamless integration with imperative constructs such as state and concurrency. Two behavioural theories are presented and studied, one based on a second-order logical relation and the other based on a polymorphic labelled transition system. The former gives a sound and complete characterisation of the contextual congruence, while the latter offers a tractable reasoning tool for a wide range of generic behaviours. The applicability of these theories is demonstrated through non-trivial reasoning examples and a fully abstract embedding of System F, the second-order polymorphic λ-calculus.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abadi, M., Cardelli, L., and Curien, P.-L. Formal parametric polymorphism. TCS 121, 1–2 (1993), 9–58.
Abramsky, S., Honda, K., and McCusker, G. Fully abstract game semantics for general reference. In LICS’98 (1998), IEEE, pp. 334–344.
Abramsky, S., and Lenisa, M. Axiomatizing fully complete models for ML polymorphic types. In Proc. of MFCS’2000 (2000).
Abramsky, S., and Lenisa, M. A fully-complete PER model for ML polymorphic types. In Proc. of CSL’2000, LNCS. Springer, 2000.
Berger, M. Towards Abstractions for Distributed Systems. PhD thesis, Imperial College, Department of Computing, 2002.
Berger, M., Honda, K., and Yoshida, N. Full version of this paper, available at www.dcs.qmul.ac.uk/~martinb,kohei and www.doc.ic.ac.uk/~yoshida.
Berger, M., Honda, K., and Yoshida, N. Sequentiality and the π-calculus. n Proc. TLCA’01 (2001), no. 2044 in LNCS, Springer, pp. 29–45.
Girard, J.-Y. Interprétation Fonctionnelle et Élimination des Coupures de l’Arithmétique d’Ordre Supérieur. PhD thesis, Universite de Paris VII, 1972.
Girard, J.-Y. Linear logic. Theoretical Computer Science 50 (1987).
Grossman, D. Existential types for imperative languages. In ESOP02 (2002), LNCS 2305, Springer, pp. 21–35.
Honda, K., and Yoshida, N. Game-theoretic analysis of call-by-value computation. TCS 221 (1999), 393–456.
Honda, K., and Yoshida, N. A uniform type structure for secure information flow. In POPL’02: A full version as DOC Report 2002/13, Imperial College, available at www.dcs.qmul.ac.uk/~kohei (2002).
Hughes, D. J. D. Games and definability for system F. In LICS’97 (1997), IEEE Computer Society Press, pp. 76–86.
Hyland, J. M. E., and Ong, C. H. L. On full abstraction for PCF. Information and Computation 163 (2000), 285–408.
Lazic, R., Newcomb, T., and Roscoe, A. On model checking data-independent systems with arrays without reset. Tech. Rep. RR-02-02, Oxford University, 2001.
Leroy, X. Polymorphic typing of an algorithmic language. PhD thesis, University of Paris, 1992.
Milner, R., Parrow, J., and Walker, D. A calculus of mobile processes, parts I and II. Info. &. Comp. 100, 1 (1992), 1–77.
Milner, R., Tofte, M., and Harper, R. W. The Definition of Standard ML. MIT Press, 1990.
Mitchell, J. C. On the equivalence of data representation. In Artificial Intelligence and Mathematical Theory of Computation (1991).
Mitchell, J. C. Foundations for Programming Languages. MIT Press, 1996.
Murawski, A., and Ong, C.-H. L. Evolving games and essential nets for afffine polymorphism. In Proc. of TLCA’01 (2001), no. 2044 in LNCS, Springer.
Pierce, B., and Sangiorgi, D. Behavioral equivalence in the polymorphic picalculus. Journal of ACM 47, 3 (2000), 531–584.
Pierce, B. C., and Turner, D. N. Pict: A programming language based on the pi-calculus. In Proof, Language and Interaction: Essays in Honour of Robin Milner, G. Plotkin, C. Stirling, and M. Tofte, Eds. MIT Press, 2000.
Pitts, A., and Stark, I. Operational reasoning for functions with local state. In HOOTS’98 (1998), CUP, pp. 227–273.
Pitts, A. M. Existential Types: Logical Relations and Operational Equivalence. In Proceedings ICALP’98 (1998), no. 1443 in LNCS, Springer, pp. 309–326.
Pitts, A. M. Parametric polymorphism and operational equivalence. Mathematical Structures in Computer Science 10 (2000), 321–359.
Plotkin, G., and Abadi, M. A logic for parameteric polymorphism. In LICS’98 (1998), IEEE Press, pp. 42–53.
Reynolds, J. C. Types, abstraction and parametric polymorphism. In Information Processing 83 (1983), R. E. A. Mason, Ed.
Tofte, M. Type inference for polymorphic references. LNCS 2305, Springer, pp. 21–35.
Turner, D. N. The Polymorphic Pi-Calculus: Theory and Implementation. PhD thesis, University of Edinburgh, 1996.
Vasconcelos, V. Typed concurrent objects. In Proceedings of ECOOP’94 (1994), LNCS, Springer, pp. 100–117.
Yoshida, N., Berger, M., and Honda, K. Strong Normalisation in the π-Calculus. In LICS’01 (2001), J. Halpern, Ed., IEEE, pp. 311–322.
Yoshida, N., Honda, K., and Berger, M. Linearity and bisimulation. In tiFoSSaCs’02 (2002), vol. 2303 of LNCS, Springer, pp. 417–433.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Berger, M., Honda, K., Yoshida, N. (2003). Genericity and the π-Calculus. In: Gordon, A.D. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2003. Lecture Notes in Computer Science, vol 2620. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36576-1_7
Download citation
DOI: https://doi.org/10.1007/3-540-36576-1_7
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00897-2
Online ISBN: 978-3-540-36576-1
eBook Packages: Springer Book Archive