Seminars details

  • FreshML: programming with binders made easy.
  • reshML extends ML with constructs for declaring and manipulating syntax with names, and also binding of names; it provides constructs for abstracting names, and pattern-matching constructs for decomposing them.<P> An abstraction is decomposed as a *fresh* name and a body (even if it was formed as a "stale" name). The freshness avoids problems such as name capture going under binders. We have recently vasty improved FreshML's usability, and programs on syntax-with-binding now look very intuitive and "just work".<P> Theoretical correctness results exist, such as one to the effect that that closed values of inductive FreshML datatypes, which may contain names and bound names, are in bijection with possibly open terms of object-level syntax up-to-alpha-equivalence.<P> However, in my talk I shall concentrate on use; what a FreshML program looks like, and how to understand the intuition behind it and how it will evaluate.
  • 28/05/2003 14:00
  • M. J. Gabbay