CakeML: A Verified Implementation of ML

The MLton repository

The Ur/Web programming language

Haskell Research Compiler

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.

The Standard ML compiler that produces Lua/JavaScript

The MaPLe compiler: efficient and scalable parallel functional programming

Moscow ML is a light-weight implementation of Standard ML (SML), a strict functional language widely used in teaching and research.

Standard ML Compiler and Toolkit

Project materials related to logic programming for interactive/reactive systems. Contains the Ceptre programming language.

The People's Refinement Logic

Standard ML of New Jersey

APL Compiler targeting a typed array intermediate language

MLWorks is a Standard ML compiler and development environment.

Generic package manager for Standard ML libraries and programs

Quantomatic is a tool for doing automated graph rewriting.

The Twelf Programming Language

SML reference interpreter

An proof refinement logic for computational type theory. Inspired by Nuprl. [For up-to-date development, see JonPRL's successor, RedPRL: https://github.com/redprl/sml-redprl]

A statically-typed programming language based on "F-ing modules"

TiML: A Functional Programming Language with Time Complexity

A small implementation of type inference

l1c is a simple formally verified compiler for a while language

A Tour of Standard ML (in the style of A Tour of Go)

Standard ML compiler based on typed intermediate languages.

A playground for parsers, type checkers, interpreters, compilers, etc.

SML On Stilts

Lexer and parser generators for Standard ML, OCaml, and Haskell.

A verified compiler for a lazy functional language