FreshML

A variant of the ML functional programming language which adds a metaprogramming facility related to higher-order abstract syntax. It provides a logical semantics for analyzing and manipulating name binding, alpha-conversion, capture avoiding substitution, and so on. Naturally, this framework provides a type-safe way to express syntactic manipulation, such as occurs with macro systems.