Stardust

Stardust is a prototype implementation of several developments in typed programming languages, most notably intersection and union types, type refinements, and first-class parametric polymorphism. Stardust is a compiler from "StardustML", a language in the Standard ML tradition, to Standard ML.

Stardust is open source software under the GPL, except for some SML/NJ-derived code, which is under a more permissive licence.

Download

Stardust

Or browse the release directory.

Stardust has dependencies on other software (principally CVC4, an SMT solver); you may need to read the installation instructions.

CVC

SML/NJ or MLton

Examples

These examples are also found in the examples subdirectory of the main distribution.

dyn Simulating dynamic typing and heterogeneous containers
overload Operator overloading
record Records
units Dimension types for unit checking
kennedy11 Dimension types for the Newton-Raphson method (adapted from Andrew Kennedy's dissertation)
kennedy66 Dimension types for exponentiation (adapted from a proposal in Andrew Kennedy's dissertation)
bool Indexed booleans and exhaustiveness checking
refine Even/odd length lists (datasort refinements)
mapfilter Simple list example
redblack Red-black tree insertion, with datasort refinements to check the colour invariant
redblue Non-value-based refinement types

Some older examples from my dissertation use a different syntax, so you won't be able to try them directly.

Papers and talks

About the "new" Stardust: About the old, never-released Stardust (a partial list):

Feedback

I welcome bug reports, comments, questions, and ideas: please send them to "jd169@" ^ "queensu" ^ ".ca". Unfortunately, my replies are likely to be neither quick nor substantive. There's no team of people working on this; there's just me.

Credits

Code

Portions of Stardust are taken from, or based on, Standard ML of New Jersey, with attribution.

Funding

Over the years, the development of Stardust has been supported, often indirectly, by the United States (particularly via the National Science Foundation), Canada, and Germany (through the Max Planck Society and the Max Planck Institute for Software Systems). These entities are, of course, not liable for this software (and according to the licence, neither am I).
J. Dunfield
Last modified: 2019-08-10