%0 Conference Proceedings
%T Type-Based Analysis for Session Inference (Extended Abstract)
%+ Trinity College Dublin
%A Spaccasassi, Carlo
%A Koutavas, Vasileios
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 36th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE)
%C Heraklion, Greece
%Y Elvira Albert
%Y Ivan Lanese
%3 Formal Techniques for Distributed Objects, Components, and Systems
%V LNCS-9688
%P 248-266
%8 2016-06-06
%D 2016
%R 10.1007/978-3-319-39570-8_17
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X We propose a type-based analysis to infer the session protocols of channels in an ML-like concurrent functional language. Combining and extending well-known techniques, we develop a type-checking system that separates the underlying ML type system from the typing of sessions. Without using linearity, our system guarantees communication safety and partial lock freedom. It also supports provably complete session inference for finite sessions with no programmer annotations. We exhibit the usefulness of our system with interesting examples, including one which is not typable in substructural type systems.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-01432922/document
%2 https://inria.hal.science/hal-01432922/file/426757_1_En_17_Chapter.pdf
%L hal-01432922
%U https://inria.hal.science/hal-01432922
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-FORTE
%~ IFIP-LNCS-9688