Channels as Objects in Concurrent Object-Oriented Programming
Joana Campos (University of Lisbon), Vasco T. Vasconcelos (University, of Lisbon)

TL;DR
This paper introduces a formal concurrent object-oriented language that uses usage types to specify protocols, object states, and method calls, enabling static verification of client code adherence in concurrent settings.
Contribution
It extends session types by removing channel operations, unifies object categories, and formalizes a type system for verifying method call correctness in concurrent object-oriented programming.
Findings
Formal language with usage types for protocols and object states
Type system enforces correct method calls and client adherence
Unified category for linear and shared objects, enabling evolution
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Advanced Software Engineering Methodologies · Distributed systems and fault tolerance
