Refinement Types for Standard ML

SML CIDRE (Checker for Intersection and Datasort Refinements)

SML CIDRE (pronounced "cider") is an implementation of a refinement-type checker for the Standard ML programming language. SML CIDRE checks properties of programs following programmer supplied annotations, and is intended to be used similarly to a type checker. However, it includes features specifically for capturing program properties, in particular intersection and datasort refinements.

Version 0.99b of SML CIDRE is available via the link below. This is a preliminary, unpublicized release: a more public release will follow shortly.

  • SML CIDRE 0.99b
    • (zip)

    Experiments

    Below are some examples of programming with refinement types in Standard ML, which were constructed while experimenting with programming using refinement types using SML CIDRE. These are included in the release of SML CIDRE above, as are a number of other examples.

  • Red-black trees:
  • red-black.sml

  • Red-black trees modified to use the simplified rotations of Okasaki:
  • red-black-okasaki.sml

  • Parsing code which resolves operator fixity and precedence, with some interesting invariants. (This code is part of the parser for the language Twelf.)
  • The main code for this example:
  • parse-term.fun

  • The rest of the code for this example, as one large file:
  • twelf-parsing-sigs.sml

  • A directory with all code, as separate files.
  • twelf-parsing/

  • A zip file with all code, and a "use" file that runs the sort checker on them in the appropriate order.
  • twelf-parsing.zip

    • Reading

    For more details, see the papers below, and my forthcoming Ph.D. dissertation.

  • Intersection Types and Computational Effects, March 2000. Proceedings of the International Conference on Functional Programming (ICFP'2000), Montreal, Canada, September 2000.  (Joint work with Frank Pfenning.)
  • Practical Refinement-Type Checking. Thesis proposal, Carnegie-Mellon University, December 1997.
  • A Practical Refinement-Type Checker for Standard ML,  Sixth International Conference on Algebraic Methodology and Software Technology (AMAST'97), Sydney, Australia, December 1997.
    •  [Note: the name "CIDRE" may be pronounced according to various local versions of "cider", including the French "cidre", and the American "sy-derh". The Australian "sy-da" is preferred in an international context.]
    Rowan Davies rowan@cs.cmu.edu Home page