Related Work

​Another bibliography by Jianzhou Zhao

Projects

These are the project pages for languages related to Disciple.

Active

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

Inactive

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.

• ​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.
• ​Inferring Method Effect Summaries for Nested Heap Regions. Vakilian, Dig, Bocchino et al, 2009.
• ​A Generic Type and Effect System. Marino, Millstein, 2009.
• ​A Capability Calculus for Concurrency and Determinism. Terauchi, Aiken, 2008.
• ​Multiple Ownership. Cameron, Drossopoulou, Noble, Smith, 2007.
• ​Protecting Representation with Effect Encapsulation. Lu, Potter, 2006.
• ​Witnessing Side Effects. Terauchi, Aiken, 2005.

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.

Tech Reports

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

• ​Types and Effects: Towards the Integration of Functional and Imperative Programming. MIT/LCS/TR-408, John M. Lucassen, August 1987.

• ​FX-87 Performance Measurements: Dataflow Implementation. MIT/LCS/TR-421, R. Todd Hammel and David K. Gifford, November 1988.