FreshML: Programming with Binders Made Simple - Erratum
Section 4 describes a certain dynamic allocation
monad on FM-cpos that is used in Section 5 to prove the main
correctness result (Theorem 5.6). The monad is specified by a
universal property (see equations (24) and (25)) and an explicit
construcion of the monad is mentioned. While a monad with that
universal property may well exist, we have discovered that our
explicit construcion for it is incorrect - and this affects our proof
of Theorem 5.6. Rather than find a correct construction for this
monad, we have found it easier to use a different, continuation-style
monad. This new (and, we think, more interesting) approach, and the
corrected proof of Theorem 5.6 using it, are described in the paper
On
a Monadic Semantics for Freshness.
Andrew Pitts
Last modified: Tue May 4 11:32:50 BST 2004