http://mw.hh.se/wg211/index.php?action=history&feed=atom&title=WG211%2FInoue 2026-04-06T00:26:21Z Revision history for this page on the wiki MediaWiki 1.43.5 http://mw.hh.se/wg211/index.php?title=WG211/Inoue&diff=665&oldid=prev 2012-06-06T19:26:02Z

<p></p> <table style="background-color: #fff; color: #202122;" data-mw="interface"> <col class="diff-marker" /> <col class="diff-content" /> <col class="diff-marker" /> <col class="diff-content" /> <tr class="diff-title" lang="en"> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">← Older revision</td> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">Revision as of 21:26, 6 June 2012</td> </tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l1">Line 1:</td> <td colspan="2" class="diff-lineno">Line 1:</td></tr> <tr><td class="diff-marker" data-marker="−"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>'''Reasoning About Multi-stage Programs''' by <del style="font-weight: bold; text-decoration: none;">Jon </del>Inoue</div></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>'''Reasoning About Multi-stage Programs''' by <ins style="font-weight: bold; text-decoration: none;">Jun </ins>Inoue</div></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>We settle three basic questions that naturally arise when verifying</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>We settle three basic questions that naturally arise when verifying</div></td></tr> </table>

Ups http://mw.hh.se/wg211/index.php?title=WG211/Inoue&diff=664&oldid=prev 2012-06-06T19:25:14Z

<p>Created page with &quot;&#039;&#039;&#039;Reasoning About Multi-stage Programs&#039;&#039;&#039; by Jon Inoue We settle three basic questions that naturally arise when verifying multi-stage functional programs. Firstly, does addin...&quot;</p> <p><b>New page</b></p><div>&#039;&#039;&#039;Reasoning About Multi-stage Programs&#039;&#039;&#039; by Jon Inoue<br /> <br /> We settle three basic questions that naturally arise when verifying<br /> multi-stage functional programs. Firstly, does adding staging to a<br /> language compromise any equalities that hold in the base language?<br /> Unfortunately it does, and more care is needed to reason about terms<br /> with free variables. Secondly, staging annotations, as the name<br /> &quot;annotations&quot; suggests, are often thought to be orthogonal to the<br /> behavior of a program, but when is this formally guaranteed to be<br /> true? We give termination conditions that characterize when this<br /> guarantee holds. Finally, do multi-stage languages satisfy useful,<br /> standard extensional facts, for example that functions agreeing on all<br /> arguments are equivalent? We provide a sound and complete notion of<br /> applicative bisimulation, which establishes such facts or, in<br /> principle, any valid program equivalence. These results greatly<br /> improve our understanding of staging, and allow us to prove the<br /> correctness of quite complicated multi-stage programs.</div>

Ups