A Message-Passing Interpretation of Adjoint Logic
We present a system of session types based on adjoint logic which generalize standard binary session types. Our system allows us to uniformly capture several new behaviors in the space of asynchronous message-passing communication, including multicast, where a process sends a single message to multi...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2019-04-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1904.01290v1 |
| _version_ | 1818146484187561984 |
|---|---|
| author | Klaas Pruiksma Frank Pfenning |
| author_facet | Klaas Pruiksma Frank Pfenning |
| author_sort | Klaas Pruiksma |
| collection | DOAJ |
| description | We present a system of session types based on adjoint logic which generalize standard binary session types. Our system allows us to uniformly capture several new behaviors in the space of asynchronous message-passing communication, including multicast, where a process sends a single message to multiple clients, replicable services, which have multiple clients and replicate themselves on-demand to handle requests from those clients, and cancellation, where a process discards a channel without communicating along it. We provide session fidelity and deadlock-freedom results for this system, from which we then derive a logically justified form of garbage collection. |
| first_indexed | 2024-12-11T12:20:05Z |
| format | Article |
| id | doaj.art-3803c46032f04a01a81f0f289dec9b09 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-11T12:20:05Z |
| publishDate | 2019-04-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-3803c46032f04a01a81f0f289dec9b092022-12-22T01:07:33ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802019-04-01291Proc. PLACES 2019607910.4204/EPTCS.291.6:8A Message-Passing Interpretation of Adjoint LogicKlaas Pruiksma0Frank Pfenning1 Carnegie Mellon University Carnegie Mellon University We present a system of session types based on adjoint logic which generalize standard binary session types. Our system allows us to uniformly capture several new behaviors in the space of asynchronous message-passing communication, including multicast, where a process sends a single message to multiple clients, replicable services, which have multiple clients and replicate themselves on-demand to handle requests from those clients, and cancellation, where a process discards a channel without communicating along it. We provide session fidelity and deadlock-freedom results for this system, from which we then derive a logically justified form of garbage collection.http://arxiv.org/pdf/1904.01290v1 |
| spellingShingle | Klaas Pruiksma Frank Pfenning A Message-Passing Interpretation of Adjoint Logic Electronic Proceedings in Theoretical Computer Science |
| title | A Message-Passing Interpretation of Adjoint Logic |
| title_full | A Message-Passing Interpretation of Adjoint Logic |
| title_fullStr | A Message-Passing Interpretation of Adjoint Logic |
| title_full_unstemmed | A Message-Passing Interpretation of Adjoint Logic |
| title_short | A Message-Passing Interpretation of Adjoint Logic |
| title_sort | message passing interpretation of adjoint logic |
| url | http://arxiv.org/pdf/1904.01290v1 |
| work_keys_str_mv | AT klaaspruiksma amessagepassinginterpretationofadjointlogic AT frankpfenning amessagepassinginterpretationofadjointlogic AT klaaspruiksma messagepassinginterpretationofadjointlogic AT frankpfenning messagepassinginterpretationofadjointlogic |