A type checking algorithm for qualified session types

Rigorous reasoning about programs calls for some amount of bureaucracy in managing details like variable binding, but, in guiding students through big ideas in semantics, we might hope to minimize the overhead. We describe our experiment introducing a range of such ideas, using the Coq proof assistant, without any explicit representation of variables, instead using a higher-order syntax encoding that we dub "mixed embedding": it is neither the fully explicit syntax of deep embeddings nor the syntax-free programming of shallow embeddings. Marquee examples include different takes on concurrency reasoning, including in the traditions of model checking (partial-order reduction), program logics (concurrent separation logic), and type checking (session types) -- all presented without any side conditions on variables.

Download Full-text

A simple library implementation of binary sessions

Journal of Functional Programming ◽

10.1017/s0956796816000289 ◽

2016 ◽

Vol 27 ◽

Cited By ~ 25

Author(s):

LUCA PADOVANI

Keyword(s):

Programming Language ◽

Protocol Analysis ◽

Simple Approach ◽

Type Inference ◽

Hybrid Form ◽

Type Checking ◽

Session Types ◽

Parametric Polymorphism ◽

Session Type

AbstractInspired by the continuation-passing encoding of binary sessions, we describe a simple approach to embed a hybrid form of session type checking into any programming language that supports parametric polymorphism. The approach combines static protocol analysis with dynamic linearity checks. To demonstrate the effectiveness of the technique, we implement a well-integrated OCaml module for session communications. For free, OCaml provides us with equirecursive session types, parametric behavioural polymorphism, complete session type inference, and session subtyping.

Download Full-text

Mixed Sessions

Programming Languages and Systems - Lecture Notes in Computer Science ◽

10.1007/978-3-030-44914-8_26 ◽

2020 ◽

pp. 715-742

Author(s):

Vasco T. Vasconcelos ◽

Filipe Casal ◽

Bernardo Almeida ◽

Andreia Mordido

Keyword(s):

Program Development ◽

Message Passing ◽

Type System ◽

The Other ◽

Runtime System ◽

Type Checking ◽

Session Types ◽

Patterns Of Interaction

AbstractSession types describe patterns of interaction on communicating channels. Traditional session types include a form of choice whereby servers offer a collection of options, of which each client picks exactly one. This sort of choice constitutes a particular case of separated choice: offering on one side, selecting on the other. We introduce mixed choices in the context of session types and argue that they increase the flexibility of program development at the same time that they reduce the number of synchronisation primitives to exactly one. We present a type system incorporating subtyping and prove preservation and absence of runtime errors for well-typed processes. We further show that classical (conventional) sessions can be faithfully and tightly embedded in mixed choices. Finally, we discuss algorithmic type checking and a runtime system built on top of a conventional (choice-less) message-passing architecture.

Download Full-text

Type checking a multithreaded functional language with session types

Theoretical Computer Science ◽

10.1016/j.tcs.2006.06.028 ◽

2006 ◽

Vol 368 (1-2) ◽

pp. 64-87 ◽

Cited By ~ 50

Author(s):

Vasco T. Vasconcelos ◽

Simon J. Gay ◽

António Ravara

Keyword(s):

Functional Language ◽

Type Checking ◽

Session Types

Download Full-text

Rast: A Language for Resource-Aware Session Types

Logical Methods in Computer Science ◽

10.46298/lmcs-18(1:9)2022 ◽

2022 ◽

Vol Volume 18, Issue 1 ◽

Author(s):

Ankush Das ◽

Frank Pfenning

Keyword(s):

Quantifier Elimination ◽

Generic Programming ◽

Concurrent Programs ◽

Program Execution ◽

Linear Arithmetic ◽

Type Checking ◽

Complexity Bounds ◽

Session Types ◽

Bidirectional Communication ◽

Resource Aware

Traditional session types prescribe bidirectional communication protocols for concurrent computations, where well-typed programs are guaranteed to adhere to the protocols. However, simple session types cannot capture properties beyond the basic type of the exchanged messages. In response, recent work has extended session types with refinements from linear arithmetic, capturing intrinsic attributes of processes and data. These refinements then play a central role in describing sequential and parallel complexity bounds on session-typed programs. The Rast language provides an open-source implementation of session-typed concurrent programs extended with arithmetic refinements as well as ergometric and temporal types to capture work and span of program execution. To further support generic programming, Rast also enhances arithmetically refined session types with recently developed nested parametric polymorphism. Type checking relies on Cooper's algorithm for quantifier elimination in Presburger arithmetic with a few significant optimizations, and a heuristic extension to nonlinear constraints. Rast furthermore includes a reconstruction engine so that most program constructs pertaining the layers of refinements and resources are inserted automatically. We provide a variety of examples to demonstrate the expressivity of the language.

Download Full-text