Version 18 (modified by benl, 7 years ago) (diff)


Related Work

Another bibliography by Jianzhou Zhao


These are the project pages for languages related to Disciple.


  • Coco uses a type-based analysis to insert monadic return and bind into an unannoted program.
  • Fstar is a language for distributed programming that carries proofs of program properties. This supersedes the F7, Fable and Fine languages, which share authors.
  • Aura also carries proofs of program properties, and is technically similar to Fstar.
  • Timber is real-time Haskell like language.
  • ATS uses dependent types to support safe pointer arithmetic and destructive update.
  • MLKit contains the original implementation of region typing as used for memory allocation and deallocation.
  • Deterministic Parallel Java has a hierarchical region typing system. The region system allows the compiler to guarantee that concurrent writes to disjoint regions do not interfere.
  • Deca is a "higher-level" assembly language with a type system inspired by Cyclone. It's in the early stages of development, but appears to work with some simple examples.


These projects appear to be dormant, based on the lack of updates to the project websites.

  • Cyclone is a type safe dialect of C using region typing and a simple effect system. This language is based on Crary, Walker and Morrisett's work on the Calculus of Capabilities (CC). Greg Morrisett moved onto the Ynot project, and Nikhil Swamy moved onto the Fstar project, both of which are languages with a focus on verification.
  • BitC is a functional language with first class mutability. From the mailing list, development seems to have been stalled by design problems in March 2011.
  • Eff was partially described in some spurious blog posts. A concrete implementation doesn't appear to have materialised.
  • FX is a historical LISP like language that implemented the original effect typing system by Gifford, Jouvelot and Lucassen.

Recent Papers

These papers are semantics papers about languages that don't appear to have concrete implementations.

Key Papers

These are key papers that introduced the main ideas used in Disciple.