Related Work

Another bibliography by Jianzhou Zhao


These are the project pages for languages related to Disciple.


  • Pawns has support for mixed pure functional and imperative programming.
  • 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.
  • 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.
  • Safe is a first order functional language with support for regions.


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

  • MLKit contains the original implementation of region typing as used for memory allocation and deallocation. The website lists Martin Elsman as the main maintainer, who has been working for a financial services company since 2008.
  • 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. This was an undergraduate honours thesis project by Eli Gottlieb, who is currently doing a PhD in Israel.
  • 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.

Tech Reports

These scanned tech reports are posted here for the good of the internet.

Last modified 3 years ago Last modified on Mar 10, 2016, 12:16:27 AM