More Web Proxy on the site http://driver.im/

Article

Types and Subtypes for Client-Server Interactions

Authors:

Malcolm HoleAuthors Info & Claims

ESOP '99: Proceedings of the 8th European Symposium on Programming Languages and Systems

Pages 74 - 90

Published: 22 March 1999 Publication History

Abstract

We define an extension of the π-calculus with a static type system which supports high-level specifications of extended patterns of communication, such as client-server protocols. Subtyping allows protocol specifications to be extended in order to describe richer behaviour; an implemented server can then be replaced by a refined implementation, without invalidating type-correctness of the overall system. We use the POP3 protocol as a concrete example of this technique.

References

[1]

G. Boudol. Asynchrony and the π-calculus (note). Rapporte de Recherche 1702, INRIA Sofia-Antipolis, May 1992.

[2]

S. J. Gay. A sort inference algorithm for the polyadic π-calculus. In Proceedings, 20th ACM Symposium on Principles of Programming Languages. ACM Press, 1993.

[3]

J.-Y. Girard. Linear Logic. Theoretical Computer Science, 50(1):1-102, 1987.

[4]

K. Honda and M. Tokoro. An object calculus for asynchronous communication. In Proceedings of the European Conference on Object-Oriented Programming, LNCS. Springer-Verlag, 1994.

[5]

K. Honda, V. Vasconcelos, and M. Kubo. Language primitives and type discipline for structured communication-based programming. In Proceedings of the European Symposium on Programming, Lecture Notes in Computer Science. Springer-Verlag, 1998.

[6]

K. Honda and N. Yoshida. Combinatory representation of mobile processes. In Proceedings, 21st ACM Symposium on Principles of Programming Languages, 1994.

[7]

N. Kobayashi. A partially deadlock-free typed process calculus. In Proceedings, Twelfth Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, 1997.

[8]

N. Kobayashi. A partially deadlock-free typed process calculus. ACM Transactions on Programming Languages and Systems, 20:436-482, 1998.

[9]

N. Kobayashi, B. C. Pierce, and D. N. Turner. Linearity and the pi-calculus. In Proceedings, 23rd ACM Symposium on Principles of Programming Languages, 1996.

[10]

I. Mackie. Lilac : A functional programming language based on linear logic. Journal of Functional Programming, 4(4):1-39, October 1994.

[11]

R. Milner. The polyadic π-calculus: A tutorial. Technical Report 91-180, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, 1991.

[12]

R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, I and II. Information and Computation, 100(1):1-77, September 1992.

[13]

J. Myers and M. Rose. Post office protocol version 3, May 1996. Internet Standards RFC1939.

[14]

O. Nierstrasz. Regular types for active objects. ACM Sigplan Notices, 28(10):1-15, October 1993.

[15]

B. Pierce and D. Sangiorgi. Types and subtypes for mobile processes. In Proceedings, Eighth Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, 1993.

[16]

B. C. Pierce and D. N. Turner. Pict: A programming language based on the pi-calculus. Technical Report CSCI 476, Computer Science Department, Indiana University, 1997. To appear in Proof, Language and Interaction: Essays in Honour of Robin Milner, Gordon Plotkin, Colin Stirling, and Mads Tofte, editors, MIT Press, 1998.

[17]

B. C. Pierce and D. N. Turner. Local type inference. In Proceedings, 25th ACM Symposium on Principles of Programming Languages, 1998.

[18]

F. Puntigam. Synchronization expressed in types of communication channels. In Proceedings of the European Conference on Parallel Processing (Euro-Par'96), volume 1123 of Lecture Notes in Computer Science. Springer-Verlag, 1996.

[19]

F. Puntigam. Coordination requirements expressed in types for active objects. In M. Aksit and S. Matsuoka, editors, Proceedings of the European Conference on Object-Oriented Programming (ECOOP'97), volume 1241 of Lecture Notes in Computer Science. Springer-Verlag, 1997.

[20]

K. Takeuchi, K. Honda, and M. Kubo. An interaction-based language and its typing system. In Proceedings of the 6th European Conference on Parallel Languages and Architectures, number 817 in Lecture Notes in Computer Science. Springer-Verlag, 1994.

[21]

D. N. Turner. The Polymorphic Pi-Calculus: Theory and Implementation. PhD thesis, University of Edinburgh, 1996.

Cited By

Thiemann PShin SShin DLencastre M(2017)Interleaving sessions with predicatesProceedings of the Symposium on Applied Computing10.1145/3019612.3019804(1312-1318)Online publication date: 3-Apr-2017
https://dl.acm.org/doi/10.1145/3019612.3019804
Lange JYoshida N(2017)On the Undecidability of Asynchronous Session SubtypingProceedings of the 20th International Conference on Foundations of Software Science and Computation Structures - Volume 1020310.1007/978-3-662-54458-7_26(441-457)Online publication date: 22-Apr-2017
https://dl.acm.org/doi/10.1007/978-3-662-54458-7_26
Lange JYoshida N(2016)Characteristic Formulae for Session TypesProceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 963610.1007/978-3-662-49674-9_52(833-850)Online publication date: 2-Apr-2016
https://dl.acm.org/doi/10.1007/978-3-662-49674-9_52
Show More Cited By

Recommendations

Shared subtypes: subtyping recursive parametrized algebraic data types
HASKELL '08

A newtype declaration in Haskell introduces a new type renaming an existing type. The two types are viewed by the programmer as semantically different, but share the same runtime representation. When operations on the two semantic views coincide, the ...
Shared subtypes: subtyping recursive parametrized algebraic data types
Haskell '08: Proceedings of the first ACM SIGPLAN symposium on Haskell

A newtype declaration in Haskell introduces a new type renaming an existing type. The two types are viewed by the programmer as semantically different, but share the same runtime representation. When operations on the two semantic views coincide, the ...
Qualified types for MLF
Proceedings of the tenth ACM SIGPLAN international conference on Functional programming

MLF is a type system that extends a functional language with impredicative rank-n polymorphism. Type inference remains possible and only in some clearly defined situations, a local type annotation is required. Qualified types are a general concept that ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

ESOP '99: Proceedings of the 8th European Symposium on Programming Languages and Systems

March 1999

304 pages

ISBN:3540656995

Editor:
S. Doaitse Swierstra

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 22 March 1999

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

29
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 07 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Thiemann PShin SShin DLencastre M(2017)Interleaving sessions with predicatesProceedings of the Symposium on Applied Computing10.1145/3019612.3019804(1312-1318)Online publication date: 3-Apr-2017
https://dl.acm.org/doi/10.1145/3019612.3019804
Lange JYoshida N(2017)On the Undecidability of Asynchronous Session SubtypingProceedings of the 20th International Conference on Foundations of Software Science and Computation Structures - Volume 1020310.1007/978-3-662-54458-7_26(441-457)Online publication date: 22-Apr-2017
https://dl.acm.org/doi/10.1007/978-3-662-54458-7_26
Lange JYoshida N(2016)Characteristic Formulae for Session TypesProceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 963610.1007/978-3-662-49674-9_52(833-850)Online publication date: 2-Apr-2016
https://dl.acm.org/doi/10.1007/978-3-662-49674-9_52
Jespersen TMunksgaard PLarsen KBahr PErdweg S(2015)Session types for RustProceedings of the 11th ACM SIGPLAN Workshop on Generic Programming10.1145/2808098.2808100(13-22)Online publication date: 30-Aug-2015
https://dl.acm.org/doi/10.1145/2808098.2808100
Gallagher JGonzalez RLocasto MGrandison THill RMaximilien M(2014)Verifying security patchesProceedings of the 2014 International Workshop on Privacy & Security in Programming10.1145/2687148.2687151(11-18)Online publication date: 21-Oct-2014
https://dl.acm.org/doi/10.1145/2687148.2687151
Yang ZZhong FZhang J(2012)A polymorphic type system with progress for binary sessionsProceedings of the 2012 international conference on Web Information Systems and Mining10.1007/978-3-642-33469-6_57(451-461)Online publication date: 26-Oct-2012
https://dl.acm.org/doi/10.1007/978-3-642-33469-6_57
Barbanera Fde'Liguoro UKutsia TSchreiner WFernández M(2010)Two notions of sub-behaviour for session-based client/server systemsProceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming10.1145/1836089.1836109(155-164)Online publication date: 26-Jul-2010
https://dl.acm.org/doi/10.1145/1836089.1836109
Bruni R(2009)Calculi for Service-Oriented ComputingFormal Methods for Web Services10.1007/978-3-642-01918-0_1(1-41)Online publication date: 22-May-2009
https://dl.acm.org/doi/10.1007/978-3-642-01918-0_1
Nanz STolstrup T(2008)Goal-oriented composition of servicesProceedings of the 7th international conference on Software composition10.5555/1793034.1793045(109-124)Online publication date: 29-Mar-2008
https://dl.acm.org/doi/10.5555/1793034.1793045
Bruni RLanese IMelgratti HTuosto E(2008)Multiparty sessions in SOCProceedings of the 10th international conference on Coordination models and languages10.5555/1788954.1788959(67-82)Online publication date: 4-Jun-2008
https://dl.acm.org/doi/10.5555/1788954.1788959
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents