articles.bib

@article{Pucella2008,
abstract = {We describe an implementation of session types in Haskell. Session types statically enforce that client-server communication proceeds according to protocols. They have been added to several concurrent calculi, but few implementations of session types are available. Our embedding takes advantage of Haskell where appropriate, but we rely on no exotic features. Thus our approach translates with minimal modification to other polymorphic, typed languages such as ML and Java. Our implementation works with existing Haskell concurrency mechanisms, handles multiple communication channels and recursive session types, and infers protocols automatically. While our implementation uses unsafe operations in Haskell, it does not violate Haskell's safety guarantees. We formalize this claim in a concurrent calculus with unsafe communication primitives over which we layer our implementation of session types, and we prove that the session types layer is safe. In particular, it enforces that channel-based communication follows consistent protocols. Copyright {\textcopyright} 2008 ACM.},
author = {Pucella, Riccardo and Tov, Jesse A.},
doi = {10.1145/1411286.1411290},
file = {:home/jmgd/Documents/work/msc/biblio/behavioral/session-types/session08.pdf:pdf},
isbn = {9781605580647},
journal = {Haskell'08 - Proceedings of the ACM SIGPLAN 2008 Haskell Symposium},
keywords = {Concurrency,Embedded type systems,Functional programming,Haskell,Phantom types,Session types,Type classes},
pages = {25--36},
title = {{Haskell session types with (almost) no class}},
year = {2008}
}
@article{Kokke2019,
abstract = {Rusty Variation (RV) is a library for session-typed communication in Rust which offers strong compile-time correctness guarantees. Programs written using RV are guaranteed to respect a specified protocol, and are guaranteed to be free from deadlocks and races.},
author = {Kokke, Wen},
doi = {10.4204/EPTCS.304.4},
file = {:home/jmgd/Documents/work/msc/biblio/behavioral/session-types/1909.05970.pdf:pdf},
issn = {20752180},
journal = {Electronic Proceedings in Theoretical Computer Science, EPTCS},
number = {Ice 2019},
pages = {48--60},
title = {{Rusty Variation Deadlock-free Sessions with Failure in Rust}},
volume = {304},
year = {2019}
}
@article{Jim2002,
abstract = {Cyclone is a safe dialect of C. It has been designed from the ground up to prevent the buffer overflows, format string attacks, and memory management errors that are common in C programs, while retaining C's syntax and semantics. This paper examines safety violations enabled by C's design, and shows how Cyclone avoids them, without giving up C's hallmark control over low-level details such as data representation and memory management.},
author = {Jim, Trevor and Morrisett, Greg and Grossman, Dan and Hicks, Michael and Cheney, James and Wang, Yanling},
file = {:home/jmgd/Documents/work/msc/biblio/behavioral/cyclone-safety.pdf:pdf},
isbn = {1880446006},
journal = {Proceedings of the 2002 USENIX Annual Technical Conference},
title = {{Cyclone: A safe dialect of C}},
year = {2002}
}
@article{Bierhoff2011,
abstract = {Objects often define usage protocols that clients must follow in order for these objects to work properly. In the presence of aliasing, however, it is difficult to check whether all the aliases of an object properly coordinate to enforce the pro-tocol. Plural is a type-based system that can soundly enforce challenging protocols even in concurrent programs. In this paper, we discuss how Plural supports natural idioms for reasoning about programs, leveraging access permissions that express the programmer's design intent within the code. We trace the predecessors of the design intent idioms used in Plural, discuss how we have found different forms of design intent to be complimentary, and outline remaining challenges and directions for future work in the area.},
author = {Bierhoff, Kevin and Beckman, Nels E. and Aldrich, Jonathan},
doi = {10.1007/978-3-642-19823-6_4},
file = {:home/jmgd/Documents/work/msc/biblio/behavioral/bierhoff-plural-festschrift11.pdf:pdf},
journal = {Engineering of Software},
pages = {35--48},
title = {{Checking Concurrent Typestate with Access Permissions in Plural: A Retrospective}},
year = {2011}
}
@article{Aldrich2016,
author = {Aldrich, Jonathan and Potanin, Alex},
file = {:home/jmgd/Documents/work/msc/biblio/dsldi16-natural.pdf:pdf},
keywords = {languages,naturally embedded domain specific},
pages = {1--2},
title = {{Naturally Embedded DSLs}},
year = {2016}
}
@article{Ekman2007,
author = {Ekman, Torbj{\"{o}}rn and Hedin, G{\"{o}}rel},
doi = {10.1145/1297105.1297029},
file = {:home/jmgd/Documents/work/msc/biblio/compiler/1297105.1297029.pdf:pdf},
keywords = {Compilers,Declarative Fra- tests in the Jacks test suite [j,Extensibility,Java like javac and the Eclipse compiler,Modularity,OOP},
number = {10},
pages = {1--18},
publisher = {Association for Computing Machinery ({\{}ACM{\}})},
title = {{The JastAdd Extensible Java Compiler}},
volume = {42},
year = {2007}
}
@article{CheckerFramework2018,
author = {{Checker Framework}},
file = {:home/jmgd/Documents/work/msc/biblio/checker-framework-manual.pdf:pdf},
number = {page 15},
pages = {253},
title = {{The Checker Framework Manual : Custom pluggable types for Java}},
url = {https://checkerframework.org/},
volume = {0},
year = {2018}
}
@book{Stroustrup1986,
abstract = {The new C++11 standard allows programmers to express ideas more clearly, simply, and directly, and to write faster, more efficient code. Bjarne Stroustrup, the designer and original implementer of C++, has reorganized, extended, and completely rewritten his definitive reference and tutorial for programmers who want to use C++ most effectively.},
author = {Stroustrup, Bjarne},
file = {:home/jmgd/Documents/work/msc/biblio/Stroustrup B. - The C++ Programming Language, 4th Edition (2013, Addison Wesley) - libgen.lc.pdf:pdf},
isbn = {978-0321563842},
pages = {1346},
title = {{The C ++ Programming}},
year = {1986}
}
@article{Honda1998,
abstract = {We introduce basic language constructs and a type discipline as a found­ation of structured communication-based concurrent programming. The constructs, which are easily translatable into the summation-less asynchronous 7r-calculus, allow programmers to organise programs as a combination of multiple flows of (possibly unbounded) reciprocal interactions in a simple and elegant way, subsuming the pre­ceding communication primitives such as method invocation and rendez-vous. The resulting syntactic structure is exploited by a type discipline a la ML, which offers a high-level type abstraction of interactive behaviours of programs as well as guar­anteeing the compatibility of interaction patterns between processes in a well-typed program. After presenting the formal semantics, the use of language constructs is illustrated through examples, and the basic syntactic results of the type discipline are established. Implementation concerns are also addressed.},
author = {Honda, Kohei and Vasconcelos, Vasco T. and Kubo, Makoto},
doi = {10.1007/bfb0053567},
file = {:home/jmgd/Documents/work/msc/biblio/behavioral/session-types/Honda1998{\_}Chapter{\_}LanguagePrimitivesAndTypeDisci.pdf:pdf},
isbn = {3540643028},
issn = {16113349},
journal = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
pages = {122--138},
title = {{Language primitives and type discipline for structured communication-based programming}},
volume = {1381},
year = {1998}
}
@article{Honda1993,
author = {Honda, Kohei},
file = {:home/jmgd/Documents/work/msc/biblio/behavioral/session-types/dyadic-inter-1993.pdf:pdf},
journal = {October},
number = {April 1992},
pages = {1--17},
title = {{Types for Dyadic Interaction 2 Typed Terms}},
year = {1993}
}
@phdthesis{Mota2020,
abstract = {Detecting programming errors and vulnerabilities in software is increasingly impor- tant, and building tools that help with this task is an area of investigation, crucial for the industry these days. When programming in an object-oriented language, one naturally defines stateful objects that are non-uniform, i.e., their methods' availability depend on their internal state. One might represent their intended usage protocol with an automaton or a state machine. Behavioral types allow to statically check if all the code of a program respects the usage protocol of each object. Mungo is a tool that extends Java with typestate definitions. These typestates are as- sociated with Java classes and define the behavior of instances of those classes, specifying the sequences of method calls allowed. The Mungo tool checks statically that method calls happen in order, following the specified behavior. Mungo misses crucial features to allow common programming practices: generics and collections are the main ones. The need for these features is illustrated by examples, like an auction that stores a collection of clients, where a usage protocol must be followed. Our goal is to define rigorously the extension to the language, develop the compiler to cope with the required functionalities, and test it with examples of realistic protocols, like Europay Mastercard Visa. Additionally, we will improve developer experience by, for instance, removing artificial restrictions that are not necessary for the verification of code, like the use of an enumeration when a boolean value is preferable. Furthermore, we will explore if the currently used frameworks, JastAdd and ExtendJ, can be replaced by a different one, for example, the Checker Framework, to increase productivity and reduce maintenance burden.},
author = {Mota, Jo{\~{a}}o},
file = {:home/jmgd/Documents/work/msc/biblio/ravara/thesis-JoaoMota.pdf:pdf},
school = {FCT-NOVA},
title = {{Coping with the reality : adding crucial features to a typestate-oriented language}},
year = {2020}
}
@inproceedings{Klabnik2016,
address = {New York, New York, USA},
author = {Klabnik, Steve},
booktitle = {Applicative 2016 on - Applicative 2016},
doi = {10.1145/2959689.2960081},
isbn = {9781450344647},
pages = {80},
publisher = {ACM Press},
title = {{The History of Rust}},
url = {http://dl.acm.org/citation.cfm?doid=2959689.2960081},
year = {2016}
}
@book{Kernighan1988,
author = {{Brian W. Kernighan}, Dennis M Ritchie},
edition = {2},
isbn = {9780131103627,0131103628},
publisher = {Prentice Hall},
title = {{The ANSI C Programming Language}},
year = {1988}
}
@article{Bezanson2017,
abstract = {Bridging cultures that have often been distant, Julia combines expertise from the diverse helds of computer science and computational science to create a new approach to numerical computing. Julia is designed to be easy and fast and questions notions generally held to be "laws of nature" by practitioners of numerical computing: 1. High-level dynamic programs have to be slow. 2. One must prototype in one language and then rewrite in another language for speed or deployment. 3. There are parts of a system appropriate for the programmer, and other parts that are best left untouched as they have been built by the experts. We introduce the Julia programming language and its design-a dance between specialization and abstraction. Specialization allows for custom treatment. Multiple dispatch, a technique from computer science, picks the right algorithm for the right circumstance. Abstraction, which is what good computation is really about, recognizes what remains the same after differences are stripped away. Abstractions in mathematics are captured as code through another technique from computer science, generic programming. Julia shows that one can achieve machine performance without sacrificing human convenience.},
archivePrefix = {arXiv},
arxivId = {1411.1607},
author = {Bezanson, Jeff and Edelman, Alan and Karpinski, Stefan and Shah, Viral B.},
doi = {10.1137/141000671},
eprint = {1411.1607},
file = {:home/jmgd/Documents/work/msc/biblio/julia-fresh-approach-BEKS.pdf:pdf},
issn = {00361445},
journal = {SIAM Review},
keywords = {Julia,Numerical,Parallel,Scientific computing},
number = {1},
pages = {65--98},
title = {{Julia: A fresh approach to numerical computing}},
volume = {59},
year = {2017}
}
@article{Coblenz2020a,
abstract = {Blockchain platforms are coming into use for processing critical transactions among participants who have not established mutual trust. Many blockchains are programmable, supporting smart contracts, which maintain persistent state and support transactions that transform the state. Unfortunately, bugs in many smart contracts have been exploited by hackers. Obsidian is a novel programming language with a type system that enables static detection of bugs that are common in smart contracts today. Obsidian is based on a core calculus, Silica, for which we proved type soundness. Obsidian uses typestate to detect improper state manipulation and uses linear types to detect abuse of assets. We integrated a permissions system that encodes a notion of ownership to allow for safe, flexible aliasing. We describe two case studies that evaluate Obsidian's applicability to the domains of parametric insurance and supply chain management, finding that Obsidian's type system facilitates reasoning about high-level states and ownership of resources. We compared our Obsidian implementation to a Solidity implementation, observing that the Solidity implementation requires much boilerplate checking and tracking of state, whereas Obsidian does this work statically.},
archivePrefix = {arXiv},
arxivId = {1909.03523},
author = {Coblenz, Michael and Oei, Reed and Etzel, Tyler and Koronkevich, Paulette and Baker, Miles and Bloem, Yannick and Myers, Brad A. and Sunshine, Joshua and Aldrich, Jonathan},
doi = {10.1145/3417516},
eprint = {1909.03523},
file = {:home/jmgd/Documents/work/msc/biblio/behavioral/typestate/obsidian.pdf:pdf},
issn = {15584593},
journal = {ACM Transactions on Programming Languages and Systems},
keywords = {Typestate,alias control,blockchain,linearity,ownership,permissions,smart contracts,type systems},
number = {3},
title = {{Obsidian: Typestate and assets for safer blockchain programming}},
volume = {42},
year = {2020}
}
@article{Yoshida2014,
abstract = {This paper describes a brief history of how Kohei Honda initiated the Scribble project, and summarises the current status of Scribble. {\textcopyright} Springer International Publishing Switzerland 2014.},
author = {Yoshida, Nobuko and Hu, Raymond and Neykova, Rumyana and Ng, Nicholas},
doi = {10.1007/978-3-319-05119-2_3},
file = {:home/jmgd/Documents/work/msc/biblio/behavioral/session-types/yoshida2014.pdf:pdf},
isbn = {9783319051185},
issn = {16113349},
journal = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
number = {October 2007},
pages = {22--41},
title = {{The scribble protocol language}},
volume = {8358 LNCS},
year = {2014}
}
@article{Coblenz2020,
author = {Coblenz, Michael and Aldrich, Jonathan and Myers, Brad A. and Sunshine, Joshua},
doi = {10.1145/3428200},
file = {:home/jmgd/Documents/work/msc/biblio/behavioral/typestate/3428200.pdf:pdf},
issn = {2475-1421},
journal = {Proceedings of the ACM on Programming Languages},
keywords = {typestate, linear types, ownership, assets, permis},
number = {OOPSLA},
pages = {1--28},
title = {{Can advanced type systems be usable? An empirical study of ownership, assets, and typestate in Obsidian}},
volume = {4},
year = {2020}
}
@book{Strom1990,
author = {Strom, Robert E and Goldberg, Arthur P and Bacon, David F and Lowry, Andy},
file = {:home/jmgd/Documents/work/msc/biblio/behavioral/typestate/hermes/Strom90HermesTutorial.pdf:pdf},
title = {{Hermes : A Tutorial and Reference Manual}},
url = {https://researcher.watson.ibm.com/researcher/files/us-bacon/Strom90HermesTutorial.pdf},
year = {1990}
}
@inproceedings{Strom1983,
address = {New York, New York, USA},
author = {Strom, Robert E.},
booktitle = {Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages - POPL '83},
doi = {10.1145/567067.567093},
file = {:home/jmgd/Documents/work/msc/biblio/behavioral/typestate/strom1983.pdf:pdf},
isbn = {0897910907},
pages = {276--284},
publisher = {ACM Press},
title = {{Mechanisms for compile-time enforcement of security}},
url = {http://portal.acm.org/citation.cfm?doid=567067.567093},
year = {1983}
}
@article{Strom1986,
abstract = {We introduce a new programming language concept called typestate, which is a refinement of the concept of type. Whereas the type of a data object determines the set of operations ever permitted on the object, typestate determines the subset of these operations which is permitted in a particular context. Typestate tracking is a program analysis technique which enhances program reliability by detecting at compile-time syntactically legal but semantically undefined execution sequences. These include, for example, reading a variable before it has been initialized, dereferencing a pointer after the dynamic object has been deallocated, etc. Typestate tracking detects errors that cannot be detected by type checking or by conventional static scope rules. Additionally, typestate tracking makes it possible for compilers to insert appropriate finalization of data at exception points and on program termination, eliminating the need to support finalization by means of either garbage collection or unsafe deallocation operations such as Pascal's dispose operation. By enforcing typestate invariants at compile-time, it becomes practical to implement a “secure language''—that is, one in which all successfully compiled program modules have fully defined execution-time effects, and the only effects of program errors are incorrect output values. This paper defines typestate, gives examples of its application, and shows how typestate checking may be embedded into a compiler. We discuss the consequences of typestate checking for software reliability and software structure, and conclude with a discussion of our experience using a high-level language incorporating typestate checking. {\textcopyright} 1986 IEEE},
author = {Strom, Robert E. and Yemini, Shaula},
doi = {10.1109/TSE.1986.6312929},
file = {:home/jmgd/Documents/work/msc/biblio/behavioral/typestate/hermes/strom1986.pdf:pdf},
issn = {00985589},
journal = {IEEE Transactions on Software Engineering},
keywords = {Program analysis,program verification,securitv,software reliability,type checking,typestate},
number = {1},
pages = {157--171},
title = {{Typestate: A Programming Language Concept for Enhancing Software Reliability}},
volume = {SE-12},
year = {1986}
}
@article{Trindade2020,
abstract = {Development of software is an iterative process. Graphical tools to represent the relevant entities and processes can be helpful. In particular, automata capture well the intended execution flow of applications, and are thus behind many formal approaches, namely behavioral types. Typestate-oriented programming allow us to model and validate the intended protocol of applications, not only providing a top-down approach to the development of software, but also coping well with compositional development. Moreover, it provides important static guarantees like protocol fidelity and some forms of progress. Mungo is a front-end tool for Java that associates a typestate describing the valid orders of method calls to each class, and statically checks that the code of all classes follows the prescribed order of method calls. To assist programming with Mungo, as typestates are textual descriptions that are terms of an elaborate grammar, we developed a tool that bidirectionally converts typestates into an adequate form of automata, providing on one direction a visualization of the underlying protocol specified by the typestate, and on the reverse direction a way to get a syntactically correct typestate from the more intuitive automata representation.},
author = {Trindade, Andr{\'{e}} and Mota, Jo{\~{a}}o and Ravara, Antonio},
doi = {10.4204/EPTCS.324.4},
file = {:home/jmgd/Documents/work/msc/biblio/behavioral/typestate/2009.08769.pdf:pdf},
issn = {20752180},
journal = {Electronic Proceedings in Theoretical Computer Science, EPTCS},
number = {Ice},
pages = {25--42},
title = {{Typestates to automata and back: A tool}},
volume = {324},
year = {2020}
}
@incollection{Toninho2013,
author = {Toninho, Bernardo and Caires, Luis and Pfenning, Frank},
doi = {10.1007/978-3-642-37036-6_20},
file = {:home/jmgd/.local/share/data/Mendeley Ltd./Mendeley Desktop/Downloaded/Toninho, Caires, Pfenning - 2013 - Higher-Order Processes, Functions, and Sessions A Monadic Integration.pdf:pdf},
pages = {350--369},
title = {{Higher-Order Processes, Functions, and Sessions: A Monadic Integration}},
url = {http://link.springer.com/10.1007/978-3-642-37036-6{\_}20},
year = {2013}
}
@article{Vasconcelos2016,
abstract = {We present here in a thorough analysis of the Mool language, covering not only its implementation but also the formalisation (syntax, operational semantics, and type system). The objective is to detect glitches in both the implementation and in the formal definitions, proposing as well new features and added expressiveness. To test our proposals we implemented the revision developed in the Racket platform.},
archivePrefix = {arXiv},
arxivId = {1604.06245},
author = {Vasconcelos, Cl{\'{a}}udio and Ravara, Ant{\'{o}}nio},
eprint = {1604.06245},
file = {:home/jmgd/Documents/work/msc/biblio/behavioral/session-types/mool/1604.06245.pdf:pdf},
pages = {1--34},
title = {{A Revision of the Mool Language}},
url = {http://arxiv.org/abs/1604.06245},
year = {2016}
}
@article{Campos2011,
abstract = {There is often a sort of a protocol associated to each class, stating when and how certain methods should be called. Given that this protocol is, if at all, described in the documentation accompanying the class, current mainstream object-oriented languages cannot provide for the verification of client code adherence against the sought class behaviour. We have defined a class-based concurrent object-oriented language that formalises such protocols in the form of usage types. Usage types are attached to class definitions, allowing for the specification of (1) the available methods, (2) the tests clients must perform on the result of methods, and (3) the object status-linear or shared-all of which depend on the object's state. Our work extends the recent approach on modular session types by eliminating channel operations, and defining the method call as the single communication primitive in both sequential and concurrent settings. In contrast to previous works, we define a single category for objects, instead of distinct categories for linear and for shared objects, and let linear objects evolve into shared ones. We introduce a standard sync qualifier to prevent thread interference in certain operations on shared objects. We formalise the language syntax, the operational semantics, and a type system that enforces by static typing that methods are called only when available, and by a single client if so specified in the usage type. We illustrate the language via a complete example.},
author = {Campos, Joana and Vasconcelos, Vasco T.},
doi = {10.4204/eptcs.69.2},
file = {:home/jmgd/Documents/work/msc/biblio/behavioral/session-types/mool/1110.4157v1.pdf:pdf},
issn = {2075-2180},
journal = {Electronic Proceedings in Theoretical Computer Science},
pages = {12--28},
title = {{Channels as Objects in Concurrent Object-Oriented Programming}},
volume = {69},
year = {2011}
}
@article{Vasconcelos2006,
abstract = {We define a language whose type system, incorporating session types, allows complex protocols to be specified by types and verified by static type checking. A session type, associated with a communication channel, specifies the state transitions of a protocol and also the data types of messages associated with transitions; thus type checking can verify both correctness of individual messages and correctness of sequences of transitions. Previously, session types have mainly been studied in the context of the $\pi$-calculus; instead, our formulation is based on a multithreaded functional language with side-effecting input/output operations. Our typing judgements statically describe dynamic changes in the types of channels, and our function types not only specify argument and result types but also describe changes in channels. We formalize the syntax, semantics and type checking system of our language, and prove subject reduction and runtime type safety theorems. {\textcopyright} 2006 Elsevier B.V. All rights reserved.},
author = {Vasconcelos, Vasco T. and Gay, Simon J. and Ravara, Ant{\'{o}}nio},
doi = {10.1016/j.tcs.2006.06.028},
file = {:home/jmgd/Documents/work/msc/biblio/behavioral/session-types/10.1016{\_}j.tcs.2006.06.028.pdf:pdf},
issn = {03043975},
journal = {Theoretical Computer Science},
keywords = {Concurrent programming,Session types,Specification of communication protocols,Static type checking},
number = {1-2},
pages = {64--87},
title = {{Type checking a multithreaded functional language with session types}},
volume = {368},
year = {2006}
}
@article{Stork2009,
abstract = {The rise of the multicore era is catapulting concurrency into mainstream programming. Current programming paradigms build in sequentiality, and as a result, concurrency support in those languages forces programmers into low-level reasoning about execution order. In this paper, we introduce a new programming paradigm in which concurrency is the default. Our Aeminium language uses access permissions to express logical dependencies in the code at a higher level of abstraction than sequential order. Therefore compiler/runtime-system can leverage that dependency information to allow concurrent execution. Because in Aeminium programmers specify dependencies rather than control flow, there is no need to engage in difficult, error-prone, and low-level reasoning about execution order or thread interleavings. Developers can instead focus on the design of the program, and benefit as the runtime automatically extracts the concurrency inherent in their design. Copyright {\textcopyright} 2009 ACM.},
author = {Stork, Sven and Marques, Paulo and Aldrich, Jonathan},
doi = {10.1145/1639950.1640060},
file = {:home/jmgd/Documents/work/msc/biblio/onward2009-concurrency.pdf:pdf},
isbn = {9781605587660},
journal = {Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA},
keywords = {Access permissions,Concurrency,Dataflow,Programming language},
pages = {933--940},
title = {{Concurrency by default: Using permissions to express dataflow in stateful programs}},
year = {2009}
}
@article{Cardelli2004,
abstract = {The fundamental purpose of a type system is to prevent the occurrence of execution errors during the running of a program. This informal statement motivates the study of type systems, but requires clarification. Its accuracy depends, first of all, on the rather subtle issue of what constitutes an execution error, which we will discuss in detail. Even when that is settled, the absence of execution errors is a nontrivial property. When such a property holds for all the program runs that can be expressed within a programming language, we say that the language is type sound. It turns out that a fair amount of careful analysis is required to avoid false and embarrassing claims of type soundness for programming languages. As a consequence, the classification, description, and study of type systems has emerged as a formal discipline.},
author = {Cardelli, Luca},
doi = {10.1201/9781420043839.ch9},
file = {:home/jmgd/Documents/work/msc/biblio/type-systems/TypeSystems.pdf:pdf},
isbn = {9780203494455},
issn = {0360-0300},
journal = {Computer Science Handbook, Second Edition},
pages = {97--1--97--32},
title = {{Type systems}},
year = {2004}
}
@book{Hopcroft2013,
author = {Hopcroft and Motwani and Ullman},
edition = {3rd},
isbn = {978-1292039053},
publisher = {Pearson},
title = {{Introduction to Automata Theory Languages, and Computation}},
year = {2013}
}
@book{Lagaillardie2020,
abstract = {Multiparty Session Types (MPST) is a typing discipline for distributed protocols, which ensures communication safety and deadlock-freedom for more than two participants. This paper reports on our research project, implementing multiparty session types in Rust. Current Rust implementations of session types are limited to binary (two-party communications). We extend an existing library for binary session types to MPST. We have implemented a simplified Amazon Prime Video Streaming protocol using our library for both shared and distributed communication transports.},
author = {Lagaillardie, Nicolas and Neykova, Rumyana and Yoshida, Nobuko},
booktitle = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
doi = {10.1007/978-3-030-50029-0_8},
file = {:home/jmgd/Documents/work/msc/biblio/behavioral/session-types/Lagaillardie2020{\_}Chapter{\_}ImplementingMultipartySessionT.pdf:pdf},
isbn = {9783030500283},
issn = {16113349},
pages = {127--136},
publisher = {Springer International Publishing},
title = {{Implementing multiparty session types in rust}},
url = {http://dx.doi.org/10.1007/978-3-030-50029-0{\_}8},
volume = {12134 LNCS},
year = {2020}
}
@article{Jespersen2015,
abstract = {We present a library for specifying session types implemented in Rust, and discuss practical use cases through examples and demonstrate how session types may be used in a large-scale application. Specifically we adapt parts of the ad-hoc communication patterns in the Servo browser engine to use session typed channels. Session types provide a protocol abstraction, expanding on traditional typed communication channels, to ensure that communication takes place according to a specified protocol. Thus, the library allows us to provide compile-time guarantees of adherence to a specific protocol without incurring significant run-time penalties.},
author = {Jespersen, Thomas Bracht Laumann and Munksgaard, Philip and Larsen, Ken Friis},
doi = {10.1145/2808098.2808100},
file = {:home/jmgd/Documents/work/msc/biblio/behavioral/session-types/laumann-munksgaard-larsen.pdf:pdf},
isbn = {9781450338103},
journal = {WGP 2015 - Proceedings of the 11th ACM SIGPLAN Workshop on Generic Programming, co-located with ICFP 2015},
keywords = {Concurrency,Generic types,Rust,Session types},
pages = {13--22},
title = {{Session types for rust}},
year = {2015}
}
@article{Gay2015,
abstract = {Session types allow communication protocols to be specified type-theoretically so that protocol implementations can be verified by static type checking. We extend previous work on session types for distributed object-oriented languages in three ways. (1) We attach a session type to a class definition, to specify the possible sequences of method calls. (2) We allow a session type (protocol) implementation to be modularized, i.e. partitioned into separately-callable methods. (3) We treat session-typed communication channels as objects, integrating their session types with the session types of classes. The result is an elegant unification of communication channels and their session types, distributed object-oriented programming, and a form of typestate supporting non-uniform objects, i.e. objects that dynamically change the set of available methods. We define syntax, operational semantics, a sound type system, and a sound and complete type checking algorithm for a small distributed class-based object-oriented language with structural subtyping. Static typing guarantees that both sequences of messages on channels, and sequences of method calls on objects, conform to type-theoretic specifications, thus ensuring type-safety. The language includes expected features of session types, such as delegation, and expected features of object-oriented programming, such as encapsulation of local state.},
author = {Gay, Simon J. and Gesbert, Nils and Ravara, Ant{\'{o}}nio and Vasconcelos, Vasco T.},
doi = {10.2168/LMCS-11(4:12)2015},
file = {:home/jmgd/Documents/work/msc/biblio/behavioral/session-types/modular-session-2015.pdf:pdf},
issn = {18605974},
journal = {Logical Methods in Computer Science},
keywords = {Non-uniform method availability,Object-oriented calculus,Session types,Typestate},
number = {4},
pages = {1--76},
title = {{Modular session types for objects}},
volume = {11},
year = {2015}
}
@article{Kouzapas2018,
abstract = {Static typechecking is an important feature of many standard programming languages. However, static typing focuses on data rather than communication, and therefore does not help programmers correctly implement communication protocols in distributed systems. The theory of session types provides a basis for tackling this problem; we use it to develop two tools that support static typechecking of communication protocols in Java. The first tool, Mungo, extends Java with typestate definitions, which allow classes to be associated with state machines defining permitted sequences of method calls: for example, communication methods. The second tool, StMungo, takes a session type describing a communication protocol, and generates a typestate specification of the permitted sequences of messages in the protocol. Protocol implementations can be validated by Mungo against their typestate definitions and then compiled with a standard Java compiler. The result is a toolchain for static typechecking of communication protocols in Java. We formalise and prove soundness of the typestate inference system used by Mungo, and show that our toolchain can be used to typecheck a client for the standard Simple Mail Transfer Protocol (SMTP).},
author = {Kouzapas, Dimitrios and Dardha, Ornela and Perera, Roly and Gay, Simon J.},
doi = {10.1016/j.scico.2017.10.006},
file = {:home/jmgd/Documents/work/msc/biblio/behavioral/session-types/mungo/1-s2.0-S0167642317302186-main.pdf:pdf},
issn = {01676423},
journal = {Science of Computer Programming},
keywords = {Object-oriented programming,Session types,Type inference,Typestate},
pages = {52--75},
publisher = {Elsevier B.V.},
title = {{Typechecking protocols with Mungo and StMungo: A session type toolchain for Java}},
url = {https://doi.org/10.1016/j.scico.2017.10.006},
volume = {155},
year = {2018}
}
@article{Vasconcelos2017,
abstract = {The widespread use of service-oriented and cloud computing is creating a need for a communication-based programming approach to distributed concurrent software systems. Protocols play a central role in the design and development of such systems but mainstream programming languages still give poor support to ensure protocol compatibility. Testing alone is insufficient to ensure it, so there is a pressing need for tools to assist the development of these kind of systems. While there are tools to verify statically objectoriented code equipped with assertions, these mainly help to prevent runtime errors. However, a program can be illbehaved and still execute without terminating abruptly. It is important to guarantee that the code implements correctly its communication protocol. Our contribution is a tool to analyse source code written in a subset of Java, equipped with assertions, and return it annotated with its respective behavioural types that can be used to verify statically that the code implements the intended protocol of the application. A running example illustrates each step of the tool.},
author = {Vasconcelos, Cl{\'{a}}udio and Ravara, Ant{\'{o}}nio},
doi = {10.1145/3019612.3019733},
file = {:home/jmgd/Documents/work/msc/biblio/behavioral/session-types/mool/3019612.3019733.pdf:pdf},
isbn = {9781450344869},
journal = {Proceedings of the ACM Symposium on Applied Computing},
keywords = {Assertions,Behavioural types,Object-oriented programming},
pages = {1492--1497},
title = {{From object-oriented code with assertions to behavioural types}},
volume = {Part F1280},
year = {2017}
}
@article{Dardha2017,
abstract = {We present two tools that support static typechecking of communication protocols in Java. Mungo associates Java classes with typestate specifications, which are state machines defining permitted sequences of method calls. StMungo translates a communication protocol specified in the Scribble protocol description language into a typestate specification for each role in the protocol by following the message sequence. Role implementations can be typechecked by Mungo to ensure that they satisfy their protocols, and then compiled as usual with javac. We demonstrate the Scribble, StMungo and Mungo toolchain via a typechecked POP3 client that can communicate with a real-world POP3 server.},
author = {Dardha, Ornela and J.Gay, Simon and Kouzapas, Dimitrios and Perera, Roly and Voinea, A. Laura and Weber, Florian},
file = {:home/jmgd/Documents/work/msc/biblio/behavioral/DGKPVW17.pdf:pdf},
isbn = {9788793519817},
journal = {Behavioural Types: from Theory to Tools English},
pages = {309--328},
title = {{Mungo and StMungo: Tools for typechecking protocols in Java}},
year = {2017}
}
@article{Voinea2020,
abstract = {This is a tutorial paper on [St]Mungo, a toolchain based on multiparty session types and their connection to typestates for safe distributed programming in Java language. The StMungo (“Scribble-to-Mungo”) tool is a bridge between multiparty session types and typestates. StMungo translates a communication protocol, namely a sequence of sends and receives of messages, given as a multiparty session type in the Scribble language, into a typestate specification and a Java API skeleton. The generated API skeleton is then further extended with the necessary logic, and finally typechecked by Mungo. The Mungo tool extends Java with (optional) typestate specifications. A typestate is a state machine specifying a Java object protocol, namely the permitted sequence of method calls of that object. Mungo statically typechecks that method calls follow the object's protocol, as defined by its typestate specification. Finally, if no errors are reported, the code is compiled with javac and run as standard Java code. In this tutorial paper we give an overview of the stages of the [St]Mungo toolchain, starting from Scribble communication protocols, translating to Java classes with typestates, and finally to typechecking method calls with Mungo. We illustrate the [St]Mungo toolchain via a real-world case study, the HTTP client-server request-response protocol over TCP. During the tutorial session, we will apply [St]Mungo to a range of examples having increasing complexity, with HTTP being one of them.},
author = {Voinea, A. Laura and Dardha, Ornela and Gay, Simon J.},
doi = {10.1007/978-3-030-50086-3_12},
file = {:home/jmgd/Documents/work/msc/biblio/behavioral/session-types/mungo/VDG20.pdf:pdf},
isbn = {9783030500856},
issn = {16113349},
journal = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
keywords = {HTTP protocol,Multiparty session types,Mungo,StMungo,Typestate},
pages = {208--224},
title = {{Typechecking java protocols with [st]mungo}},
volume = {12136 LNCS},
year = {2020}
}
@inproceedings{Aldrich2009,
address = {New York, New York, USA},
author = {Aldrich, Jonathan and Sunshine, Joshua and Saini, Darpan and Sparks, Zachary},
booktitle = {Proceeding of the 24th ACM SIGPLAN conference companion on Object oriented programming systems languages and applications - OOPSLA '09},
doi = {10.1145/1639950.1640073},
file = {:home/jmgd/Documents/work/msc/biblio/behavioral/typestate/onward2009-state.pdf:pdf},
isbn = {9781605587684},
pages = {1015},
publisher = {ACM Press},
title = {{Typestate-oriented programming}},
url = {http://www.cs.cmu.edu/{~}aldrich/papers/onward2009-state.pdf http://dl.acm.org/citation.cfm?doid=1639950.1640073},
year = {2009}
}
@article{DeLine2004,
abstract = {Even in a safe programming language, such as C♯ or Java, disobeying the rules for using an interface can cause exceptions at run time. Such rules govern how system resources are managed, the order of method calls, and the formatting of string parameters, such as SQL queries. This paper introduces Fugue, a modular static checker for languages that compile to the Common Language Runtime. Fugue allows the rules for using an interface to be recorded as declarative specifications and provides a range of annotations that allow a developer to specify interface rule with varying precision. At the simplest end of the range, a specifier can mark those methods that allocate and release resources. A specifier can also limit the order in which an object's methods may be called to the transitions of a finite state machine. At the most complex end of the range, a specifier can give a method a plug-in pre- and postconditon, which is arbitrary code that examines an object's current state and a static approximation of the method's actuals, decides whether the call is legal and returns the object's state after the call. We used these features to specify rules for using ADO.NET, a library for accessing relational databases, and found several errors in an internal Microsoft Research web site, which extensively uses this library.},
author = {DeLine, Robert and F{\"{a}}hndrich, Manuel},
file = {:home/jmgd/Documents/work/msc/biblio/behavioral/typestate/fugue-2004.pdf:pdf},
journal = {Submitted manuscript},
number = {January},
title = {{The Fugue protocol checker: Is your software Baroque?}},
url = {http://research.microsoft.com/apps/pubs/default.aspx?id=67458{\%}5Cnhttp://research.microsoft.com/en-us/projects/fugue/},
year = {2004}
}
@article{Ancona2016,
abstract = {A recent trend in programming language research is to use behavioral type theory to ensure various correctness properties of large-scale, communication-intensive systems. Behavioral types encompass concepts such as interfaces, communication protocols, contracts, and choreography. The successful application of behavioral types requires a solid understanding of several practical aspects, from their representation in a concrete programming language, to their integration with other programming constructs such as methods and functions, to design and monitoring methodologies that take behaviors into account. This survey provides an overview of the state of the art of these aspects, which we summarize as the pragmatics of behavioral types.},
author = {Ancona, Davide and Bono, Viviana and Bravetti, Mario and Campos, Joana and Castagna, Giuseppe and Deni{\'{e}}lou, Pierre Malo and Gay, Simon J. and Gesbert, Nils and Giachino, Elena and Hu, Raymond and Johnsen, Einar Broch and Martins, Francisco and Mascardi, Viviana and Montesi, Fabrizio and Neykova, Rumyana and Ng, Nicholas and Padovani, Luca and Vasconcelos, Vasco T. and Yoshida, Nobuko},
doi = {10.1561/2500000031},
file = {:home/jmgd/Documents/work/msc/biblio/behavioral/ancona2016.pdf:pdf},
issn = {23251131},
journal = {Foundations and Trends in Programming Languages},
number = {2-3},
pages = {95--230},
title = {{Behavioral types in programming languages}},
volume = {3},
year = {2016}
}
@book{Gay2017,
abstract = {Behavioural type systems in programming languages support the specification and verification of properties of programs beyond the traditional use of type systems to describe data processing. A major example of such a property is correctness of communication in concurrent and distributed systems, motivated by the importance of structured communication in modern software. Behavioural Types: from Theory to Tools presents programming languages and software tools produced by members of COST Action IC1201: Behavioural Types for Reliable Large-Scale Software Systems, a European research network that was funded from October 2012 to October 2016. As a survey of the most recent developments in the application of behavioural type systems, it is a valuable reference for researchers in the field, as well as an introduction to the area for graduate students and software developers.},
author = {Gay, Simon and Ravara, Ant{\'{o}}nio},
booktitle = {Behavioural Types: from Theory to Tools English},
doi = {10.13052/rp-9788793519817},
file = {:home/jmgd/Documents/work/msc/biblio/behavioral/RE{\_}9788793519817.pdf:pdf},
isbn = {9788793519817},
pages = {1--375},
title = {{Behavioural types: From theory to tools english}},
year = {2017}
}
@article{Fahndrich2002,
abstract = {A type system with linearity is useful for checking software protocols and resource management at compile time. Linearity provides powerful reasoning about state changes, but at the price of restrictions on aliasing. The hard division between linear and nonlinear types forces the programmer to make a trade-off between checking a protocol on an object and aliasing the object. Most onerous is the restriction that any type with a linear component must itself be linear. Because of this, checking a protocol on an object imposes aliasing restrictions on any data structure that directly or indirectly points to the object. We propose a new type system that reduces these restrictions with the adoption and focus constructs. Adoption safely allows a programmer to alias objects on which she is checking protocols, and focus allows the reverse. A programmer can alias data structures that point to linear objects and use focus for safe access to those objects. We discuss how we implemented these ideas in the Vault programming language.},
author = {F{\"{a}}hndrich, Manuel and DeLine, Robert},
doi = {10.1145/543552.512532},
file = {:home/jmgd/Documents/work/msc/biblio/behavioral/fahndrichdeline02adoptionfocus.pdf:pdf},
isbn = {1581134630},
issn = {1558-1160},
journal = {Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)},
keywords = {Heap aliasing,Linear types,Region-based memory management},
pages = {13--24},
title = {{Adoption and focus: Practical linear types for imperative programming}},
year = {2002}
}
@article{DeLine2004a,
abstract = {Today's mainstream object-oriented compilers and tools do not support declaring and statically checking simple pre- and postconditions on methods and invariants on object representations. The main technical problem preventing static verification is reasoning about the sharing relationships among objects as well as where object invariants should hold. We have developed a programming model of typestates for objects with a sound modular checking algorithm. The programming model handles typical aspects of object-oriented programs such as downcasting, virtual dispatch, direct calls, and subclassing. The model also permits subclasses to extend the interpretation of typestates and to introduce additional typestates. We handle aliasing by adapting our previous work on practical linear types developed in the context of the Vault system. We have implemented these ideas in a tool called Fugue for specifying and checking typestates on Microsoft .NET-based programs. {\textcopyright} Springer-Verlag 2004.},
author = {Deline, Robert and F{\"{a}}hndrich, Manuel},
doi = {10.1007/978-3-540-24851-4_21},
file = {:home/jmgd/Documents/work/msc/biblio/behavioral/typestate/deline-typestates.pdf:pdf},
isbn = {354022159X},
issn = {16113349},
journal = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
pages = {465--490},
title = {{Typestates for Objects}},
volume = {3086},
year = {2004}
}
@article{Hu2008,
abstract = {This paper demonstrates the impact of integrating session types and object-oriented programming, through their implementation in Java. Session types provide high-level abstraction for structuring a series of interactions in a concise syntax, and ensure type-safe communications between distributed peers. We present the first full implementation of a language and runtime for session-based distributed programming featuring asynchronous message passing, delegation, and session subtyping and interleaving, combined with class downloading and failure handling. The compilation-runtime framework of our language effectively maps session abstraction onto underlying transports and guarantees communication safety through static and dynamic session type checking. We have implemented two alternative mechanisms for performing distributed session delegation and prove their correctness. Benchmark results show session abstraction can be realised with low runtime overhead. {\textcopyright} 2008 Springer-Verlag.},
author = {Hu, Raymond and Yoshida, Nobuko and Honda, Kohei},
doi = {10.1007/978-3-540-70592-5_22},
file = {:home/jmgd/Documents/work/msc/biblio/behavioral/session-types/hu07-sessionj.pdf:pdf},
isbn = {3540705910},
issn = {03029743},
journal = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
pages = {516--541},
title = {{Session-based distributed programming in Java}},
volume = {5142 LNCS},
year = {2008}
}
@article{Huttel2016,
abstract = {Behavioural type systems, usually associated to concurrent or distributed computations, encompass concepts such as interfaces, communication protocols, and contracts, in addition to the traditional input/output operations. The behavioural type of a software component specifies its expected patterns of interaction using expressive type languages, so types can be used to determine automatically whether the component interacts correctly with other components. Two related important notions of behavioural types are those of session types and behavioural contracts. This article surveys the main accomplishments of the last 20 years within these two approaches.},
author = {H{\"{u}}ttel, Hans and Lanese, Ivan and Vasconcelos, Vasco T. and Caires, L{\'{u}}is and Carbone, Mmarco and Deni{\'{e}}lou, Pierre Malo and Mostrous, Dimitris and Padovani, Luca and Ni{\'{o}}ravara, Ant{\'{o}} and Tuosto, Emilio and Vieira, Hugo Torres and Zavattaro, Gianluigi},
doi = {10.1145/2873052},
file = {:home/jmgd/Documents/work/msc/biblio/behavioral/session-types/2873052.pdf:pdf},
issn = {15577341},
journal = {ACM Computing Surveys},
keywords = {Behavioural types},
number = {1},
pages = {1--36},
title = {{Foundations of session types and behavioural contracts}},
volume = {49},
year = {2016}
}
@article{Garcia2014,
author = {Garcia, Ronald and Tanter, {\'{E}}ric and Wolff, Roger and Aldrich, Jonathan},
doi = {10.1145/2629609},
file = {:home/jmgd/Documents/work/msc/biblio/behavioral/typestate/10.1145{\_}2629609.pdf:pdf},
issn = {0164-0925},
journal = {ACM Transactions on Programming Languages and Systems},
month = {oct},
number = {4},
pages = {1--44},
title = {{Foundations of Typestate-Oriented Programming}},
url = {https://dl.acm.org/doi/10.1145/2629609},
volume = {36},
year = {2014}
}
@article{Padovani2011,
abstract = {We propose a semantically grounded theory of session types which relies on intersection and union types. We argue that intersection and union types are natural candidates for modeling branching points in session types and we show that the resulting theory overcomes some important defects of related behavioral theories. In particular, intersections and unions provide a native solution to the problem of computing joins and meets of session types. Also, the subtyping relation turns out to be a pre-congruence, while this is not always the case in related behavioral theories.},
author = {Padovani, Luca},
doi = {10.4204/eptcs.45.6},
file = {:home/jmgd/Documents/work/msc/biblio/behavioral/session-types/1101.4429.pdf:pdf},
issn = {2075-2180},
journal = {Electronic Proceedings in Theoretical Computer Science},
number = {Itrs 2010},
pages = {71--89},
title = {{Session Types = Intersection Types + Union Types}},
volume = {45},
year = {2011}
}
@article{Xi2016a,
abstract = {Traditionally, each party in a (dyadic or multiparty) session implements exactly one role specified in the type of the session. We refer to this kind of session as an individual session (i-session). As a generalization of i-session, a group session (g-session) is one in which each party may implement a group of roles based on one channel. In particular, each of the two parties involved in a dyadic g-session implements either a group of roles or its complement. In this paper, we present a formalization of g-sessions in a multi-threaded lambda-calculus (MTLC) equipped with a linear type system, establishing for the MTLC both type preservation and global progress. As this formulated MTLC can be readily embedded into ATS, a full-fledged language with a functional programming core that supports both dependent types (of DML-style) and linear types, we obtain a direct implementation of linearly typed g-sessions in ATS. The primary contribution of the paper lies in both of the identification of g-sessions as a fundamental building block for multiparty sessions and the theoretical development in support of this identification.},
archivePrefix = {arXiv},
arxivId = {1604.03020},
author = {Xi, Hongwei and Wu, Hanwen},
eprint = {1604.03020},
file = {:home/jmgd/Documents/work/msc/biblio/behavioral/session-types/ats/1604.03020.pdf:pdf},
keywords = {Computer Science - Programming Languages},
title = {{Linearly Typed Dyadic Group Sessions for Building Multiparty Sessions}},
year = {2016}
}
@article{Xi2016,
abstract = {We present a formalization of session types in a multi-threaded lambda-calculus (MTLC) equipped with a linear type system, establishing for the MTLC both type preservation and global progress. The latter (global progress) implies that the evaluation of a well-typed program in the MTLC can never reach a deadlock. As this formulated MTLC can be readily embedded into ATS, a full-fledged language with a functional programming core that supports both dependent types (of DML-style) and linear types, we obtain a direct implementation of session types in ATS. In addition, we gain immediate support for a form of dependent session types based on this embedding into ATS. Compared to various existing formalizations of session types, we see the one given in this paper is unique in its closeness to concrete implementation. In particular, we report such an implementation ready for practical use that generates Erlang code from well-typed ATS source (making use of session types), thus taking great advantage of the infrastructural support for distributed computing in Erlang.},
archivePrefix = {arXiv},
arxivId = {1603.03727},
author = {Xi, Hongwei and Ren, Zhiqiang and Wu, Hanwen and Blair, William},
eprint = {1603.03727},
file = {:home/jmgd/Documents/work/msc/biblio/behavioral/session-types/ats/1603.03727.pdf:pdf},
keywords = {Computer Science - Logic in Computer Science,Computer Science - Programming Languages},
title = {{Session Types in a Linearly Typed Multi-Threaded Lambda-Calculus}},
year = {2016}
}