PICT (2365/pic016)


is a language in the ML tradition, formed by adding a layer of convenient syntactic sugar and a static type system to a tiny core. The current release includes a PICT-to-C compiler, reference manual, tutorial, libraries for common data structures, example programs, and a rudimentary X-based widget toolkit. The core language, an asynchronous variant of Milner, Parrow, and Walker's pi-calculus, has been used as a theoretical foundation for a broad class of concurrent computations.
The goal is to identify high-level idioms that arise naturally when these primitives are used to build working programs, idioms such as basic data structures, protocols for returning results, higher-order programming, selective communication and concurrent objects. Developed by Benjamin Pierce, University of Cambridge.

Places
Structures:
Related languages
Pi Calculus => PICT   Based on
PICT => Piccola   Influence

References:
  • Turner, David N, "The Polymorphic Pi-Calculus: Theory and Implications" PhD Thesis Edinburgh 1995 view details External link: Online copy Abstract: We investigate whether the Pi-calculus is able to serve as a good foundation for the design and implementation of a strongly-typed concurrent programming language.  The first half of the dissertation examines whether the Pi-calculus supports a simple  type system which is flexible enough to provide a suitable foundation for the type  system of a concurrent programming language. The second half of the dissertation  considers how to implement the Pi-calculus efficiently, starting with an abstract  machine for Pi-calculus and finally presenting a compilation of Pi-calculus to C.  We start the dissertation by presenting a simple, structural type system for  Pi-calculus, and then, after proving the soundness of our type system, show how  to infer principal types for Pi-terms. This simple type system can be extended  to include useful type-theoretic constructions such as recursive types and higher-  order polymorphism. Higher-order polymorphism is important, since it gives  us the ability to implement abstract datatypes in a type-safe manner, thereby  providing a greater degree of modularity for Pi-calculus programs.

    The functional computational paradigm plays an important part in many programming languages. It is well-known that the Pi-calculus can encode functional computation. We go further and show that the type structure of ^-terms is preserved by such encodings, in the sense that we can relate the type of a ^-term to  the type of its encoding in the Pi-calculus. This means that a Pi-calculus programming language can genuinely support typed functional programming as a special  case.

    An efficient implementation of Pi-calculus is necessary if we wish to consider Pi-calculus as an operational foundation for concurrent programming. We first give a simple abstract machine for Pi-calculus and prove it correct. We then show how  this abstract machine inspires a simple, but efficient, compilation of Pi-calculus to C (which now forms the basis of the Pict programming language implementation).
  • Walker, David "Objects and the pi-calculus" Information and Computation, 1995. view details
  • Pierce, Benjamin C. and Turner, David N. "Pict Language Definition", Version 3.9d, 1996 view details
  • Pierce, Benjamin C. and Turner, David N. Pict: A programming language based on the pi-calculus. Technical report, Computer Science Department, Indiana University, 1997. To appear in Milner festschrift, MIT Press. view details
  • Achermann, Franz "JPict - a framework for pi Agents" Technical Report, IAM, U. Bern, November 1998, tech. note view details ps
    Resources
    • Page for PICT at U Penn
      external link

    • Current binaries and sources

      "