Version 8 (modified by benl, 8 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 A language for distributed programming that carries proofs of program properties
  • Timber A real-time Haskell like language.
  • MLKit A ML compiler using region typing. I believe this work contains the original implementation of region typing as used for memory allocation and deallocation.
  • Deterministic Parallel Java A Java dialect with a hierarchical region typing system. The region system allows the type system to guarantee that concurrent writes to disjoint regions do not interfere.


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

  • Cyclone 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. A functional language with first class mutability.
  • Eff. Some spurious blog posts about a new language with effect typing that doesn't appear to have materialised into an implementation.
  • FX The original effect typing system.

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.