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