FreshML extends ML with constructs for declaring and manipulating abstract syntax trees that involve statically scoped binders. FreshML is impure, in the sense that fresh name generation is an observable side effect, and lexically unsafe, in the sense that it allows the construction of abstract syntax trees that unintentionally contain unbound names.

Following in the steps of early work by Pitts and Gabbay, I will present Pure FreshML, a version of FreshML equipped with a static proof system that guarantees purity and lexical safety. Pure FreshML relies on a rich "binding specification'' language, borrowed from alphaCaml, on user-provided assertions (guards, preconditions, and postconditions), and on a conservative, automatic decision procedure for a logic that allows reasoning about values and about the names that they contain.

I will show that non-trivial syntax-manipulating algorithms can be expressed in Pure FreshML. I hope that this result could have an impact on the design of FreshML, MetaML, and other meta-programming languages.