Pict: A Programming Language Based on the Pi-Calculus
Benjamin C. Pierce, David N. Turner · The MIT Press eBooks · 2000
The ß-calculus offers an attractive basis for concurrent programming. It is small, elegant, and well studied, and supports (via simple encodings) a wide range of high-level constructs including data structures, higher-order functional programming, concurrent control structures, and objects. Moreover, familiar type systems for the -calculus have direct counterparts in the ß-calculus, yielding strong, static typing for a high-level language using the ß-calculus as its core. This paper describes Pict, a strongly-typed concurrent programming language constructed in terms of an explicitly-typed ß-calculus core language. Dedicated to Robin Milner on the occasion of his 60th birthday. 1 Introduction Milner, Parrow, and Walker's ß-calculus [MPW92, Mil91] generalizes the channel-based communication of CCS and its relatives by allowing channels to be passed as data along other channels. This extension introduces an element of mobility, enabling the specification and verification of concurrent ...