Sciweavers

LICS
2007
IEEE

Static Name Control for FreshML

14 years 6 months ago
Static Name Control for FreshML
FreshML extends ML with constructs for declaring and ting abstract syntax trees that involve names and statically scoped binders. It is impure: name generation is an observable side effect. In practice, this means that FreshML allows writing programs that create fresh names and unintentionally fail to bind them. Following in the steps of early work by Pitts and Gabbay, this paper defines Pure FreshML, a subset of FreshML equipped with a static proof system that guarantees purity. Pure FreshML relies on a rich binding specification language, on user-provided assertions, expressed in a logic that allows reasoning about values and about the names that they contain, and on a conservative, automatic decision procedure for this logic. It is argued that Pure FreshML can express non-trivial syntaxmanipulating algorithms.
François Pottier
Added 04 Jun 2010
Updated 04 Jun 2010
Type Conference
Year 2007
Where LICS
Authors François Pottier
Comments (0)