Related Work

​Another bibliography by Jianzhou Zhao

Projects

These are the project pages for languages related to Disciple.

Active

• ​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.

Inactive

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.

• ​A Flexible Semantic Framework for Effects. Tate, Leijen, Lerner, 2011 (submitted).
• ​Type Inference with Natural Subtyping. Tate, Leijen, 2010.
• ​Relational Semantics for Effect Based Program Transformations. Benton, Beringer, Hofmann, Kennedy, 2009.
• ​Witnessing Side Effects. Terauchi, Aiken, 2005.
• ​A Generic Type and Effect System. Marino, Millstein, 2009.
• ​A Capability Calculus for Concurrency and Determinism. Terauchi, Aiken, 2008.
• ​Inferring Method Effect Summaries for Nested Heap Regions. Vakilian, Dig, Bocchino et al, 2009.
• ​Multiple Ownership. Cameron, Drossopoulou, Noble, Smith, 2007.
• ​Protecting Representation with Effect Encapsulation. Lu, Potter, 2006.

Key Papers

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

• ​Polymorphic Effect Systems. Foundations for region and effect typing. Lucassen, Gifford, 1988.
• ​The Type and Effect Discipline. Core of DDC's type inference algorithm, and namesake. Talpin, Jouvelot, 1992.
• ​Polymorphic Typing of an Algorithmic Language. Foundations for closure typing. Leroy, 1992.
• ​The Calculus of Capabilities. Foundations for DDC's core language. Walker, Crary, Morrisett, 2000.