| Abstract
|
<p>We settle three basic questions t … <p>We settle three basic questions that naturally arise when verifying multi-stage functional programs. Firstly, does adding staging to a language compromise any equalities that hold in the base language? Unfortunately it does, and more care is needed to reason about terms with free variables. Secondly, staging annotations, as the name “annotations” suggests, are often thought to be orthogonal to the behavior of a program, but when is this formally guaranteed to be true? We give termination conditions that characterize when this guarantee holds. Finally, do multi-stage languages satisfy useful, standard extensional facts—for example, that functions agreeing on all arguments are equivalent? We provide a sound and complete notion of applicative bisimulation, which establishes such facts or, in principle, any valid program equivalence. These results greatly improve our understanding of staging, and allow us to prove the correctness of quite complicated multi-stage programs.</p>omplicated multi-stage programs.</p>
|
| Author
|
Jun Inoue +
, Walid Taha +
|
| Conference
|
21st European Symposium on Programming, ESOP 2012, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn 24 March-1 April
|
| DOI
|
http://dx.doi.org/10.1007/978-3-642-28869-2_18 +
|
| Diva
|
http://hh.diva-portal.org/smash/record.jsf?searchId=1&pid=diva2:488415
|
| EndPage
|
376 +
|
| HostPublication
|
Proceedings of the 22nd European Symposium on Programming (ESOP 2012) +
|
| PublicationType
|
Conference Paper +
|
| Publisher
|
Springer Publishing Company +
|
| Series
|
Lecture Notes in Computer Science ; 7211 +
|
| StartPage
|
357 +
|
| Title
|
Reasoning About Multi-Stage Programs +
|
| Year
|
2012 +
|
| Has queryThis property is a special property in this wiki.
|
Publications:Reasoning About Multi-Stage Programs +
, Publications:Reasoning About Multi-Stage Programs +
, Publications:Reasoning About Multi-Stage Programs +
, Publications:Reasoning About Multi-Stage Programs +
, Publications:Reasoning About Multi-Stage Programs +
, Publications:Reasoning About Multi-Stage Programs +
, Publications:Reasoning About Multi-Stage Programs +
, Publications:Reasoning About Multi-Stage Programs +
, Publications:Reasoning About Multi-Stage Programs +
, Publications:Reasoning About Multi-Stage Programs +
|
| Categories |
Publication +
|
| Modification dateThis property is a special property in this wiki.
|
26 June 2014 03:44:54 +
|
