Merge pull request #249 from the-au-forml-lab/paper-vote-3

Message-Observing Sessions

data/desc.txt

@@ -1,3 +1,3 @@
-Embedding by Unembedding
-Matsuda, Kazutaka, et al. “Embedding by Unembedding.” Proceedings of the ACM on Programming Languages, vol. 7, no. ICFP, Aug. 2023, pp. 1–47. Crossref, https://doi.org/10.1145/3607830.
-Embedding is a language development technique that implements the object language as a library in a host language. There are many advantages of the approach, including being lightweight and the ability to inherit features of the host language. A notable example is the technique of HOAS, which makes crucial use of higher-order functions to represent abstract syntax trees with binders. Despite its popularity, HOAS has its limitations. We observe that HOAS struggles with semantic domains that cannot be naturally expressed as functions, particularly when open expressions are involved. Prominent examples of this include incremental computation and reversible/bidirectional languages. In this paper, we pin-point the challenge faced by HOAS as a mismatch between the semantic domain of host and object language functions, and propose a solution. The solution is based on the technique of unembedding , which converts from the finally-tagless representation to de Bruijn-indexed terms with strong correctness guarantees. We show that this approach is able to extend the applicability of HOAS while preserving its elegance. We provide a generic strategy for Embedding by Unembedding, and then demonstrate its effectiveness with two substantial case studies in the domains of incremental computation and bidirectional transformations. The resulting embedded implementations are comparable in features to the state-of-the-art language implementations in the respective areas.
+Message-Observing Sessions
+Kavanagh, Ryan, and Brigitte Pientka. “Message-Observing Sessions.” Proceedings of the ACM on Programming Languages, vol. 8, no. OOPSLA1, Apr. 2024, pp. 1351–79. Crossref, https://doi.org/10.1145/3649859.
+We present Most, a process language with message-observing session types. Message-observing session types extend binary session types with type-level computation to specify communication protocols that vary based on messages observed on other channels. Hence, Most allows us to express global invariants about processes, rather than just local invariants, in a bottom-up, compositional way. We give Most a semantic foundation using traces with binding, a semantic approach for compositionally reasoning about traces in the presence of name generation. We use this semantics to prove type soundness and compositionality for Most processes. We see this as a significant step towards capturing message-dependencies and providing more precise guarantees about processes.

data/history.txt

@@ -38,4 +38,5 @@ https://doi.org/10.1145/3622820
 https://doi.org/10.1145/3632907
 https://doi.org/10.1017/S0956796824000017
 https://doi.org/10.1145/3689739
-https://doi.org/10.1145/3607830
+https://doi.org/10.1145/3607830
+https://doi.org/10.1145/3649859

data/next.txt

@@ -1 +1 @@
-https://doi.org/10.1145/3607830
+https://doi.org/10.1145/3649859

data/past.txt

@@ -1,4 +1,5 @@
 
 https://doi.org/10.1017/S0956796824000017
 https://doi.org/10.1145/3689739
-https://doi.org/10.1145/3607830
+https://doi.org/10.1145/3607830
+https://doi.org/10.1145/3649859

docs/index.md

@@ -25,7 +25,7 @@ The PL Reading Group is a regular meeting of [ΔΛΔ](https://augusta.presence.i
 | 1.  | January 17  | Knuth–Morris–Pratt illustrated  | UH 227 |
 | 2.  | January 24  | Fully Verified Instruction Scheduling  | TBD |
 | 3.  | January 31  | Embedding by Unembedding  | UH 227 |
-| 4.  | February 7  | Paper 4 discussion  | UH 227 |
+| 4.  | February 7  | Message-Observing Sessions  | UH 227 |
 | 5.  | February 14 | Paper 5 discussion  | UH 227 |
 | 6.  | February 21 | Paper 6 discussion  | UH 227 |
 | 7.  | February 28 | Paper 7 discussion  | UH 227 |

docs/papers.md

@@ -1,3 +1,4 @@
 1. MOY, CAMERON. “Knuth–Morris–Pratt Illustrated.” Journal of Functional Programming, vol. 34, 2024. Crossref, <a href='https://doi.org/10.1017/S0956796824000017' target='_blank'>https://doi.org/10.1017/S0956796824000017</a>.
 2. Yang, Ziteng, et al. “Fully Verified Instruction Scheduling.” Proceedings of the ACM on Programming Languages, vol. 8, no. OOPSLA2, Oct. 2024, pp. 791–816. Crossref, <a href='https://doi.org/10.1145/3689739' target='_blank'>https://doi.org/10.1145/3689739</a>.
-3. Matsuda, Kazutaka, et al. “Embedding by Unembedding.” Proceedings of the ACM on Programming Languages, vol. 7, no. ICFP, Aug. 2023, pp. 1–47. Crossref, <a href='https://doi.org/10.1145/3607830' target='_blank'>https://doi.org/10.1145/3607830</a>.
+3. Matsuda, Kazutaka, et al. “Embedding by Unembedding.” Proceedings of the ACM on Programming Languages, vol. 7, no. ICFP, Aug. 2023, pp. 1–47. Crossref, <a href='https://doi.org/10.1145/3607830' target='_blank'>https://doi.org/10.1145/3607830</a>.
+4. Kavanagh, Ryan, and Brigitte Pientka. “Message-Observing Sessions.” Proceedings of the ACM on Programming Languages, vol. 8, no. OOPSLA1, Apr. 2024, pp. 1351–79. Crossref, <a href='https://doi.org/10.1145/3649859' target='_blank'>https://doi.org/10.1145/3649859</a>.