Here is a list of companies, projects, and courses that use or have used MLton. If you use MLton and are not here, please add your project with a brief description and a link. Thanks.
Companies
-
Hardcore Processing uses MLton as a crosscompiler from Linux to Windows for graphics and game software.
-
CEX3D Converter, a conversion program for 3D objects.
-
Interactive Showreel, which contains a crossplatform GUI-toolkit and a realtime renderer for a subset of RenderMan written in Standard ML.
-
various games
-
-
MathWorks/PolySpace Technologies builds their product that detects runtime errors in embedded systems based on abstract interpretation.
-
Reactive Systems uses MLton to build Reactis, a model-based testing and validation package used in the automotive and aerospace industries.
Projects
-
ADATE, Automatic Design of Algorithms Through Evolution, a system for automatic programming i.e., inductive inference of algorithms. ADATE can automatically generate non-trivial and novel algorithms written in Standard ML.
-
CIL, a compiler for SML based on intersection and union types.
-
ConCert, a project investigating certified code for grid computing.
-
Guugelhupf, a simple search engine.
-
HaMLet, a model implementation of Standard ML.
-
Heron, a discrete-event simulation solver for polychronous timed systems
-
KeplerCode, independent verification of the computational aspects of proofs of the Kepler conjecture and the Dodecahedral conjecture.
-
Metis, a first-order prover (used in the HOL4 theorem prover and the Isabelle theorem prover).
-
mlftpd, an ftp daemon written in SML. TomMurphy is also working on replacements for standard network services in SML. He also uses MLton to build his entries (2001, 2002, 2004, 2005) in the annual ICFP programming contest.
-
MLOPE, an offline partial evaluator for Standard ML.
-
RML, a system for developing, compiling and debugging and teaching structural operational semantics (SOS) and natural semantics specifications.
-
Skalpel, a type-error slicer for SML
-
SSA PRE, an implementation of Partial Redundancy Elimination for MLton.
-
Stabilizers, a modular checkpointing abstraction for concurrent functional programs.
-
Self-Adjusting SML, self-adjusting computation, a model of computing where programs can automatically adjust to changes to their data.
-
TL System, providing general-purpose support for rewrite-based transformation over elements belonging to a (user-defined) domain language.
-
Tina (Time Petri net Analyzer)
-
Twelf an implementation of the LF logical framework.
-
WaveScript/WaveScript, a sensor network project; the WaveScript compiler can generate SML (MLton) code.
Courses
-
Harvard CS-152, undergraduate programming languages.
-
Høgskolen i Østfold IAI30202, programming languages.