Email Gateway (Aug 19 2022 at 10:19): Email Gateway (Aug 19 2022 at 10:19):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
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.
[http://afp.sf.net/entries/Launchbury.shtml]
Enjoy,
Gerwin
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.
Last updated: Apr 16 2024 at 20:15 UTC