Parameterized Algebraic Protocols

2023/04/07 by Andreia Mordido, Janek Spaderna, Peter Thiemann +1 · 1 voice
Computer Science · Mathematics · #Algebraic number #Algorithm #Computer science #Context (archaeology) #Formal Methods in Verification #Logic, programming, and type systems #Mathematics #Modularity (biology) #Parameterized complexity #Programming language #Protocol (science) #Session (web analytics) #Software Engineering Research #Template #Theoretical computer science #cs.PL

paper · pdf · doi:10.1145/3591277

arxiv published 2023/04/07 · arxiv updated 2023/04/07 · openalex publication_date 2023/06/06 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

We propose algebraic protocols that enable the definition of protocol templates and session types analogous to the definition of domain-specific types with algebraic datatypes. Parameterized algebraic protocols subsume all regular as well as most context-free and nested session types and, at the same time, replace the expensive superlinear algorithms for type checking by a nominal check that runs in linear time. Algebraic protocols in combination with polymorphism increase expressiveness and modularity by facilitating new ways of parameterizing and composing session types.

Citations

• Linear Haskell: practical linearity in a higher-order polymorphic language
• Higher-order Context-free Session Types in System F
• Linear Logic, the π-calculus, and their Metatheory: A Recipe for Proofs as Processes

Discussions

• An Formalism arxiv.org/abs/2304.03764 [bsky, 0 points, 0 comments]

Related

• A simple library implementation of binary sessions
• Session Types with Arithmetic Refinements
• Polymorphic Lambda Calculus with Context-Free Session Types
• Domain-Aware Session Types (Extended Version)
• Session Coalgebras: A Coalgebraic View on Session Types and Communication Protocols