A Sound Reduction Semantics for Untyped CBN Multi-Stage Computation: Or, the Theory of MetaML is Non-trivial (Extended Abstract)
2000 (English)In: PEPM '00: Proceedings of the 2000 ACM SIGPLAN workshop on Partial evaluation and semantics-based program manipulation, New York, NY: ACM Press, 2000, Vol. 34, p. 34-43Conference paper, Published paper (Refereed)
Abstract [en]
A multi-stage computation is one involving more than one stage of execution. MetaML is a language for programming multi-stage computations. Previous studies presented big-step semantics, categorical semantics, and sound type systems for MetaML. In this paper, we report on a confluent and sound reduction semantics for untyped call-by name (CBN) MetaML. The reduction semantics can be used to formally justify some optimization performed by a CBN MetaML implementation. The reduction semantics demonstrates that non-trivial equalities hold for object-code, even in the untyped setting. The paper also emphasizes that adding intensional analysis (that is, taking-apart object programs) to MetaML remains an interesting open problem. © 2000 ACM, Inc.
Place, publisher, year, edition, pages
New York, NY: ACM Press, 2000. Vol. 34, p. 34-43
Series
ACM / SIGPLAN Notices, ISSN 0362-1340 ; 11
National Category
Computer Systems
Identifiers
URN: urn:nbn:se:hh:diva-20991DOI: 10.1145/328691.328697ISI: 000084855700007Scopus ID: 2-s2.0-0033691593Libris ID: 12438393ISBN: 1-58113-201-8 OAI: oai:DiVA.org:hh-20991DiVA, id: diva2:588299
Conference
PEPM'00 – International Symposium on Partial Evaluation and Semantics Based Program Manipulation, Boston, MA, USA, 22-23 January, 2000
Funder
Swedish Research Council
Note
The research reported in this paper was carried out at the Pacific Software Research Center (PacSoft), Department of Computer Science and Engineering, Oregon Graduate Institute of Science & Technology, Portland, OR, USA, and was supported by the USAF Air Materiel Command, contract # F19628-93-C-0069, and NSF Grant IRI-9625462. The paper is based on results presented in the author's PhD dissertation. Author is currently a Post-doctoral Fellow supported by the Swedish Research Council for Engineering Sciences (TFR), grant number 221-96-403.
2013-01-152013-01-142021-05-11Bibliographically approved