Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Reasoning About Multi-Stage Programs
Rice University, Houston, Texas, USA. (Department of Computer Science)
Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES). Rice University, Houston, Texas, USA.
2012 (English)In: Programming Languages and Systems: 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings / [ed] Helmut Seidl, Berlin: Springer Publishing Company, 2012, Vol. 7211, 357-376 p.Conference paper, Published paper (Refereed)
Abstract [en]

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. © 2012 Springer-Verlag.

Place, publisher, year, edition, pages
Berlin: Springer Publishing Company, 2012. Vol. 7211, 357-376 p.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 7211
Keyword [en]
Multi-stage programming, verification, bisimulation
National Category
Language Technology (Computational Linguistics)
Identifiers
URN: urn:nbn:se:hh:diva-17088DOI: 10.1007/978-3-642-28869-2_18ISI: 000310871200018Scopus ID: 2-s2.0-84859129520Libris ID: 13428714ISBN: 978-3-642-28868-5 (print)OAI: oai:DiVA.org:hh-17088DiVA: diva2:488415
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, 2012
Available from: 2012-02-06 Created: 2012-02-01 Last updated: 2017-05-02Bibliographically approved

Open Access in DiVA

reasoning-about-msp(436 kB)223 downloads
File information
File name FULLTEXT01.pdfFile size 436 kBChecksum SHA-512
0102a6ca865981c71e8a1654c0b7e87cce493c4f9cb14f80e768c69584d3513acd09d81c076c236db0ba42a18f7a3af5b263a130ad93d30c65afef83ebad9602
Type fulltextMimetype application/pdf

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Inoue, JunTaha, Walid
By organisation
Centre for Research on Embedded Systems (CERES)
Language Technology (Computational Linguistics)

Search outside of DiVA

GoogleGoogle Scholar
Total: 223 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 152 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf