Home   >   CSC-OpenAccess Library   >    Manuscript Information
Principal Type Scheme for Session Types
Alvaro Tasistro, Ernesto Copello, Nora Szasz
Pages - 34 - 43     |    Revised - 15-11-2012     |    Published - 31-12-2012
Volume - 3   Issue - 1    |    Publication Date - October 2012  Table of Contents
MORE INFORMATION
KEYWORDS
Types, Principal Type Scheme, Type Inference Algorithm
ABSTRACT
Session types model communication between processes as dialogues speci ed by sequences of types of messages, each of which describe the format and direction of the message. The resulting system imposes a type discipline that guarantees compatibility of interaction patterns between processes of a well-typed program. The system is polymorphic in Curry\'s style, but no formal treatment of this aspect has been provided yet. In this paper we present a system assigning type schemes to programs and an algorithm of inference of the principal type scheme of any typable program for a signifi cant fragment of the calculus which allows delegation of communication, i.e. transmission of channels. We use classical syntax for variables and channels, i.e. just one sort of names in each case for either bound or free occurrences. We prove soundness and completeness of the algorithm, working on individual terms rather than on alpha -equivalence classes. The algorithm has been implemented in Haskell and partially checked in the proof assistant Agda.
CITED BY (5)  
1 Bjerregaard, M. O., Poulsen, N. S., & Wahl, S. (2016, May). Type Inference for Session Types in the π-calculus. In Web Services, Formal Methods, and Behavioral Types: 11th International Workshop, WS-FM 2014, Eindhoven, The Netherlands, September 11-12, 2014, and 12th International Workshop, WS-FM/BEAT 2015, Madrid, Spain, September 4-5, 2015, Revise
2 Hüttel, H., Lanese, I., Vasconcelos, V. T., Caires, L., Carbone, M., Deniélou, P. M., ... & Vieira, H. T. (2016). Foundations of session types and behavioural contracts. ACM Computing Surveys (CSUR), 49(1), 3.
3 Lanese, I., Vasconcelos, V. T., Caires, L., Carbone, M., Deniélou, P. M., Mostrous, D., ... & Zavattaro, G. Hans Hüttel, Aalborg University.
4 Graversen, E. F., Harbo, J. B., Hüttel, H., Bjerregaard, M. O., Poulsen, N. S., & Wahl, S. (2014). Type Inference for Session Types in the pi-calculus. In Web Services, Formal Methods, and Behavioral Types (pp. 103-121). Springer International Publishing.
5 Copello, E. (2012). Inferencia de tipos de sesión (Doctoral dissertation, Master’s thesis, Universidad ORT Uruguay).
1 Google Scholar 
2 CiteSeerX 
3 refSeek 
4 Scribd 
5 SlideShare 
6 PdfSR 
Ernesto Copello. Inferencia de tipos de sesión. Master’s thesis, Universidad ORT Uruguay,2012.
F. Cardone and M. Coppo. “Type inference with recursive types: Syntax and semantics”. Inf.Comput., 92(1):48–80, 1991.
K. Honda, V. T. Vasconcelos, and M. Kubo. “Language primitives and type disciplines for structured communication-based programming”. In ESOP’98, volume 1381 of LNCS, pages 22–138. Springer, 1998.
K. Honda. “Types for dyadic interaction”. In Eike Best, editor, CONCUR’93, volume 715 of Lecture Notes in Computer Science, pages 509–523. Springer Berlin / Heidelberg, 1993.10.1007/3-540-57208-2_35.
K. Takeuchi, K. Honda, and M. Kubo. “An interaction-based language and its typing system”. In Constantine Halatsis, Dimitris G. Maritsas, George Philokyprou, and Sergios Theodoridis,editors, PARLE, volume 817 of Lecture Notes in Computer Science, pages 398–413. Springer,1994.
L. G. Mezzina. “How to infer finite session types in a calculus of services and sessions”. In Proceedings of the 10th international conference on Coordination models and languages,COORDINATION’08, pages 216–231, Berlin, Heidelberg, 2008. Springer-Verlag.
M. Neubauer and P. Thiemann. “An implementation of session types”. In Bharat Jayaraman,editor, PADL, volume 3057 of Lecture Notes in Computer Science, pages 56–70. Springer,2004.
M. P. Jones. “Type classes with functional dependencies”. In Proceedings of the 9th European Symposium on Programming Languages and Systems, ESOP ’00, pages 230–244, London,UK, 2000. Springer-Verlag.
M. Sackman and S. Eisenbach. “Session Types in Haskell: Updating Message Passing for the 21st Century”. Technical report, June 2008.
N. Yoshida and V. T. Vasconcelos. “Language primitives and type discipline for structured communication-based programming revisited: Two systems for higher-order session communication”. In 1st International Workshop on Security and Rewriting Techniques, volume 171(4) of ENTCS, pages 73–93. Elsevier, 2007.
R. Pucella and J. A. Tov. “Haskell session types with (almost) no class”. SIGPLAN Not.,44(2):25–36, September 2008.
S. J. Gay and M. Hole. “Subtyping for session types in the pi calculus”. Acta Inf., pages 191–225, 2005.
U. Norell. “Towards a practical programming language based on dependent type theory”. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology,SE-412 96 Göteborg, Sweden, September 2007.
Dr. Alvaro Tasistro
- Uruguay
tasistro@ort.edu.uy
Mr. Ernesto Copello
- Uruguay
Miss Nora Szasz
- Uruguay


CREATE AUTHOR ACCOUNT
 
LAUNCH YOUR SPECIAL ISSUE
View all special issues >>
 
PUBLICATION VIDEOS