• Before proceeding ...

    Please note that Dependent ML (DML) is no longer under active development. As a language, it has already been fully incorporated into ATS.

  • What is DML?

    Dependent ML (DML) is a conservative extension of the functional programming language ML. The type system of DML enriches that of ML with a restricted form of dependent types. This allows many interesting program properties such as memory safety and termination to be captured in the type system of DML and then be verified at compiler-time.

  • Some sample DML and de Caml code:

  • More Examples:

    Please find more and larger DML examples here and de Caml examples here.

  • Thesis on Dependent ML:

    Hongwei Xi, Dependent Types in Practical Programming, Ph.D thesis, Carnegie Mellon University, pp viii+187, September, 1998.

  • Papers on or related to Dependent ML:

  • Implementation:

  • DML The current (undocumented) implementation of a DML type-checker can be found here, which is written in Objective Caml. Please follow the file session.txt to install it. The syntax of DML can be readily learned from the various examples included in the distribution given that one is already familiar with Standard ML. Also, termination checking is supported in this implementation.

  • de Caml We have implemented de Caml, which essentially is the Caml-light compiler extended with a front-end supporting DML style dependent types. An undocumented distribution is already released. There are various examples available along with the distribution. We expect that one should have no difficulty using deCaml if he or she is familiar with Caml-light.

  • Comments are welcome