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

A visualisation of polymorphic type checking

2000 ◽  
Vol 10 (1) ◽  
pp. 57-75 ◽  
Author(s):  
YANG JUNG ◽  
GREG MICHAELSON
Keyword(s):  
Functional Language ◽  
Type Checking ◽  
Standard Ml ◽  
Graphical Environment ◽  
Polymorphic Type

The understanding of polymorphic typechecking and type errors is poorly supported by contemporary functional language implementations. Here, a novel visualisation of functions and their types is presented based on the generation of function specific icons with graphical type representations which change dynamically as functions are applied. This visualisation has been implemented for a Standard ML subset within a graphical environment in which function combinations are constrained by type matching.

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 Propositions as sessions

2014 ◽  
Vol 24 (2-3) ◽  
pp. 384-418 ◽  
Author(s):  
PHILIP WADLER
Keyword(s):  
Linear Functional ◽  
Linear Logic ◽  
Functional Language ◽  
Session Types ◽  
Deadlock Freedom ◽  
First Time ◽  
Standard Presentation

AbstractContinuing a line of work by Abramsky (1994), Bellin and Scott (1994), and Caires and Pfenning (2010), among others, this paper presents CP, a calculus, in which propositions of classical linear logic correspond to session types. Continuing a line of work by Honda (1993), Hondaet al. (1998), and Gay & Vasconcelos (2010), among others, this paper presents GV, a linear functional language with session types, and a translation from GV into CP. The translation formalises for the first time a connection between a standard presentation of session types and linear logic, and shows how a modification to the standard presentation yields a language free from races and deadlock, where race and deadlock freedom follows from the correspondence to linear logic.

scholarly journals FreeST: Context-free Session Types in a Functional Language

2019 ◽  
Vol 291 ◽  
pp. 12-23
Author(s):  
Bernardo Almeida ◽  
Andreia Mordido ◽  
Vasco T. Vasconcelos
Keyword(s):  
Functional Language ◽  
Session Types ◽  
Context Free

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 A type system for extracting functional specifications from memory-safe imperative programs

2021 ◽  
Vol 5 (OOPSLA) ◽  
pp. 1-29
Author(s):  
Paul He ◽  
Eddy Westbrook ◽  
Brent Carmer ◽  
Chris Phifer ◽  
Valentin Robert ◽  
...  
Keyword(s):  
Type System ◽  
Functional Language ◽  
Memory Safety ◽  
Type Checking ◽  
Significant Time ◽  
Functional Specification

Verifying imperative programs is hard. A key difficulty is that the specification of what an imperative program does is often intertwined with details about pointers and imperative state. Although there are a number of powerful separation logics that allow the details of imperative state to be captured and managed, these details are complicated and reasoning about them requires significant time and expertise. In this paper, we take a different approach: a memory-safe type system that, as part of type-checking, extracts functional specifications from imperative programs. This disentangles imperative state, which is handled by the type system, from functional specifications, which can be verified without reference to pointers. A key difficulty is that sometimes memory safety depends crucially on the functional specification of a program; e.g., an array index is only memory-safe if the index is in bounds. To handle this case, our specification extraction inserts dynamic checks into the specification. Verification then requires the additional proof that none of these checks fail. However, these checks are in a purely functional language, and so this proof also requires no reasoning about pointers.

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.

Sign in / Sign up

Export Citation Format

Share Document