scholarly journals Rast: A Language for Resource-Aware Session Types

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.

scholarly journals Skipping the binder bureaucracy with mixed embeddings in a semantics course (functional pearl)

2021 ◽  
Vol 5 (ICFP) ◽  
pp. 1-28
Author(s):  
Adam Chlipala
Keyword(s):  
Order Reduction ◽  
Separation Logic ◽  
Variable Binding ◽  
Type Checking ◽  
Session Types ◽  
The Coq Proof Assistant ◽  
Reduction Program ◽  
Coq Proof Assistant ◽  
Big Ideas ◽  
Concurrent Separation Logic

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.

A simple library implementation of binary sessions

2016 ◽  
Vol 27 ◽  
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.

scholarly journals Steel: proof-oriented programming in a dependently typed concurrent separation logic

2021 ◽  
Vol 5 (ICFP) ◽  
pp. 1-30
Author(s):  
Aymeric Fromherz ◽  
Aseem Rastogi ◽  
Nikhil Swamy ◽  
Sydney Gibson ◽  
Guido Martínez ◽  
...  
Keyword(s):  
Linked Data ◽  
Separation Logic ◽  
Concurrent Programs ◽  
Interactive Proof ◽  
First Order ◽  
Session Types ◽  
Verification Condition ◽  
New Formulation ◽  
Concurrent Separation Logic ◽  
Efficient Verification

Steel is a language for developing and proving concurrent programs embedded in F ⋆ , a dependently typed programming language and proof assistant. Based on SteelCore, a concurrent separation logic (CSL) formalized in F ⋆ , our work focuses on exposing the proof rules of the logic in a form that enables programs and proofs to be effectively co-developed. Our main contributions include a new formulation of a Hoare logic of quintuples involving both separation logic and first-order logic, enabling efficient verification condition (VC) generation and proof discharge using a combination of tactics and SMT solving. We relate the VCs produced by our quintuple system to solving a system of associativity-commutativity (AC) unification constraints and develop tactics to (partially) solve these constraints using AC-matching modulo SMT-dischargeable equations. Our system is fully mechanized and implemented in F ⋆ . We evaluate it by developing several verified programs and libraries, including various sequential and concurrent linked data structures, proof libraries, and a library for 2-party session types. Our experience leads us to conclude that our system enables a mixture of automated and interactive proof, making it productive to build programs foundationally verified against a highly expressive, state-of-the-art CSL.

scholarly journals Resource-Aware Session Types for Digital Contracts

2021 ◽  
Author(s):  
Ankush Das ◽  
Stephanie Balzer ◽  
Jan Hoffmann ◽  
Frank Pfenning ◽  
Ishani Santurkar
Keyword(s):  
Session Types ◽  
Resource Aware

scholarly journals Mixed Sessions

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.

scholarly journals Type checking a multithreaded functional language with session types

2006 ◽  
Vol 368 (1-2) ◽  
pp. 64-87 ◽  
Author(s):  
Vasco T. Vasconcelos ◽  
Simon J. Gay ◽  
António Ravara
Keyword(s):  
Functional Language ◽  
Type Checking ◽  
Session Types
Sign in / Sign up

Export Citation Format

Share Document