hh.sePublications
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
National Institute of Advanced Industrial Science and Technology, Ikeda, Osaka, Japan.
Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES).ORCID iD: 0000-0003-3160-9188
2016 (English)In: Journal of functional programming (Print), ISSN 0956-7968, E-ISSN 1469-7653, Vol. 26, article id e22Article in journal (Refereed) Published
Abstract [en]

We settle three basic questions that naturally arise when verifying code generators written in multi-stage functional programming languages. First, 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. Second, 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 properties, for example, that functions agreeing on all arguments are equivalent? We provide a sound and complete notion of applicative bisimulation, which establishes such properties or, in principle, any valid program equivalence. These results yield important insights into staging and allow us to prove the correctness of quite complicated multi-stage programs. © Cambridge University Press 2016.

Place, publisher, year, edition, pages
Cambridge: Cambridge University Press, 2016. Vol. 26, article id e22
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:hh:diva-35686DOI: 10.1017/S0956796816000253ISI: 000388093800001Scopus ID: 2-s2.0-84994106379OAI: oai:DiVA.org:hh-35686DiVA, id: diva2:1183877
Note

Funding: NSF CCF 0747431 award entitled “Multi-stage programming for object-oriented languages”, NSF CSR/EHS 0720857 award entitled “Building physically safe embedded systems”, NSF CPS 1136099 award entitled “A CPS Approach to Robot Design”, and Halmstad University.

Available from: 2018-02-19 Created: 2018-02-19 Last updated: 2018-02-19Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

Taha, Walid

Search in DiVA

By author/editor
Taha, Walid
By organisation
Centre for Research on Embedded Systems (CERES)
In the same journal
Journal of functional programming (Print)
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 119 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