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
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
For more details, see the papers below, and my forthcoming
[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 firstname.lastname@example.org