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


Related Work

Another bibliography by Jianzhou Zhao


These are the project pages for other languages related to Disciple.

  • Fstar A language for distributed programming that carries proofs of program properties
  • Cyclone A type safe dialect of C using region typing and capabilities. Grossman, Hicks, Jim, Morrisett, Swamy, Wang et al. (active)
  • Timber A real-time Haskell like language. Nordlander et al. (active)
  • MLKit A ML compiler using region typing. Elsman, Hallenberg, Varming, Tofte, Birkedal et al. (active)
  • Eff. Bauer, Pretnar. (inactive?)
  • BitC. A functional language with first class mutability. Shapiro, Sridhar, Doerrie. (inactive?)
  • FX The original effect typing system. Gifford, Jouvelot et al. (inactive)

Recent Papers

If you know of other recent work on effects, region typing, controlling mutability, or capability calculi then please add it here. We are particularly interested in systems that can express the noninterference of concurrent threads in their type systems, while not requiring all data to be constant (as in Haskell), and not adding intermediate messaging protocols (as in Erlang or with STM).

Semantics and Program Transformation

Ownership typing in Object Oriented Languages

Key Papers