[isabelle] new AFP entry: Launchbury

The following new entry is now available from http://afp.sf.net

The Correctness of Launchbury's Natural Semantics for Lazy Evaluation
by Joachim Breitner

In his seminal paper „Natural Semantics for Lazy Evaluation“, John
Launchbury proves his semantics correct with respect to a denotational
semantics. We have formalized both semantics and identified an ambiguity
in what the operator ⊔ should do: If it is understood as the least upper
bound, as hinted at in the paper, the original proof fails. We fix the
proof by taking a detour via a modified natural semantics with an
explicit stack. In addition, we show that the original proof goes
through when ⊔ is understood to be right-sided update.




The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.