More Like this

1. Domain-Aware Session Types

   https://doi.org/doi.org/10.4230/LIPIcs.CONCUR.2019.39  

   Caires, Luis; Perez, Jorge A.; Pfenning, Frank; Toninho, Bernardo (August 2019, Leibniz international proceedings in informatics)

   null (Ed.)
2. Probabilistic Refinement Session Types

   https://doi.org/10.1145/3729317  

   Fu, Qiancheng; Das, Ankush; Gaboardi, Marco (June 2025, Proceedings of the ACM on Programming Languages)

   Session types provide a formal type system to define and verify communication protocols between message-passing processes. In order to analyze randomized systems, recent works have extended session types with probabilistic type constructors. Unfortunately, all the proposed extensions only support constant probabilities which limits their applicability to real-world systems. Our work addresses this limitation by introducing probabilistic refinement session types which enable symbolic reasoning for concurrent probabilistic systems in a core calculus we call PReST. The type system is carefully designed to be a conservative extension of refinement session types and supports both probabilistic and regular choice type operators. We also implement PReST in a prototype which we use for validating probabilistic concurrent programs. The added expressive power leads to significant challenges, both in the meta theory and implementation of PReST, particularly with type checking: it requires reconstructing intermediate types for channels when type checking probabilistic branching expressions. The theory handles this by semantically quantifying refinement variables in probabilistic typing rules, a deviation from standard refinement type systems. The implementation relies on a bi-directional type checker that uses an SMT solver to reconstruct the intermediate types minimizing annotation overhead and increasing usability. To guarantee that probabilistic processes are almost-surely terminating, we integrate cost analysis into our type system to obtain expected upper bounds on recursion depth. We evaluate PReST on a wide variety of benchmarks from 4 categories: (i) randomized distributed protocols such as Itai and Rodeh's leader election, bounded retransmission, etc., (ii) parametric Markov chains such as random walks, (iii) probabilistic analysis of concurrent data structures such as queues, and (iv) distributions obtained by composing uniform distributions using operators like max, and sum. Our experiments show that the PReST type checker scales to large programs with sophisticated probabilistic distributions. 

   more » « less
3. Session Types with Arithmetic Refinements

   https://doi.org/https://doi.org/10.4230/LIPIcs.CONCUR.2020.13  

   Das, Ankush; Pfenning, Frank (August 2020, 31st International Conference on Concurrency Theory (CONCUR 2020))

   null (Ed.)
4. Manifest sharing with session types

   https://doi.org/10.1145/3110281  

   Balzer, Stephanie; Pfenning, Frank (August 2017, Proceedings of the ACM on Programming Languages)
5. Probabilistic Resource-Aware Session Types

   https://doi.org/10.1145/3571259  

   Das, Ankush; Wang, Di; Hoffmann, Jan (January 2023, Proceedings of the ACM on Programming Languages)

   Session types guarantee that message-passing processes adhere to predefined communication protocols. Prior work on session types has focused on deterministic languages but many message-passing systems, such as Markov chains and randomized distributed algorithms, are probabilistic. To implement and analyze such systems, this article develops the meta theory of probabilistic session types with an application focus on automatic expected resource analysis. Probabilistic session types describe probability distributions over messages and are a conservative extension of intuitionistic (binary) session types. To send on a probabilistic channel, processes have to utilize internal randomness from a probabilistic branching or external randomness from receiving on a probabilistic channel. The analysis for expected resource bounds is smoothly integrated with the type system and is a variant of automatic amortized resource analysis. Type inference relies on linear constraint solving to automatically derive symbolic bounds for various cost metrics. The technical contributions include the meta theory that is based on a novel nested multiverse semantics and a type-reconstruction algorithm that allows flexible mixing of different sources of randomness without burdening the programmer with complex type annotations. The type system has been implemented in the language NomosPro with linear-time type checking. Experiments demonstrate that NomosPro is applicable in different domains such as cost analysis of randomized distributed algorithms, analysis of Markov chains, probabilistic analysis of amortized data structures and digital contracts. NomosPro is also shown to be scalable by (i) implementing two broadcast and a bounded retransmission protocol where messages are dropped with a fixed probability, and (ii) verifying the limiting distribution of a Markov chain with 64 states and 420 transitions. 

   more » « less