Название: Session TypesАвтор: Simon J. Gay, Vasco T. Vasconcelos
Издательство: Cambridge University Press
Год: 2025
Страниц: 247
Язык: английский
Формат: pdf
Размер: 10.1 MB
The topic of session types concerns the use of programming language type systems to specify and verify the communication behaviour of programs. Just as data types describe the structure of data and constrain the operations that can be performed on it, session types describe the structure of communication and constrain the communication operations that can be performed. A session type is a formal description of a communication protocol, made accessible to programming language tools such as typecheckers, compilers, IDEs and runtime monitors.
Session types are type-theoretic specifications of communication protocols in concurrent or distributed systems. By codifying the structure of communication, they make software more reliable and easier to construct. Over recent decades, the topic has become a large and active research area within the field of programming language theory and implementation. Written by leading researchers in the field, this is the first text to provide a comprehensive introduction to the key concepts of session types. The thorough theoretical treatment is complemented by examples and exercises, suitable for use in a lecture course or for self-study. It serves as an entry point to the topic for graduate students and researchers.
Programming languages allow data structures to be codified as data types, and programming tools and environments use data types as the basis for analysis and verification. This could be at compile time, in languages such as Java, C, Scala and Haskell, or at run time, in languages such as Python. In a typical integrated development environment (IDE) such as Eclipse, writing code that applies an operation to the wrong data type (for example, calling a method that doesn’t exist in a class) produces a visual highlight of the error (such as a × or an underline). Clicking on the error then produces a menu suggesting operations that can be validly applied.
Session types are type-theoretic specifications of communication protocols, so that protocol implementations can be verified by compile-time type checking in a programming language. We can introduce the key ideas through a series of examples. An extremely simple protocol specifies sending one message, which is an integer, and then closing the connection.
‘This book on session types, one of most fruitful and successful topics in concurrency theory over the past 30 years, is written with great clarity, deep insight, and enthusiasm by two of most renowned researchers in the field. It is a most welcomed text, both for learning from and for teaching. It offers a comprehensive account of the basic theory and explains the possible applications, beautifully leavened with insightful examples and exercises. It will become -- and well deserves to become - the definitive reference textbook on session types.’ Davide Sangiorgi, University of Bologna
‘How should we structure distributed computation? One of the most promising approaches is Session Types. Here we have a superb introduction by two founders of the field. Gay and Vasconcelos provide a readable yet thorough introduction. It has long been needed, and will help the field flourish.’ Philip Wadler, University of Edinburgh
‘This book offers a deep view on the core theory of binary session types. The reader is captivated by the appropriate and clarifying examples and stimulated by the challenging exercises. The authors are outstanding researchers as witnessed by the simplicity and rigour of their writing.’ Mariangiola Dezani-Ciancaglini, University of Turin
‘Session types codify communication structures of concurrent and distributed programs, guiding the programmer to write type and communication safe programs. This book explains binary session types starting from basics to advance, making it accessible to students, newcomers and programmers at the industry alike.’ Nobuko Yoshida, University of Oxford
Скачать Session Types