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