A sound reduction semantics for untyped CBN multi-stage computation. Or, the theory of MetaML is non-trival
- 1 November 1999
- journal article
- Published by Association for Computing Machinery (ACM) in ACM SIGPLAN Notices
- Vol. 34 (11) , 34-43
- https://doi.org/10.1145/328691.328697
Abstract
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.Keywords
This publication has 16 references indexed in Scilit:
- MetaML and multi-stage programming with explicit annotationsTheoretical Computer Science, 2000
- Multi-stage programming: axiomatization and type safetyPublished by Springer Nature ,1998
- A computational formalization for partial evaluationMathematical Structures in Computer Science, 1997
- Sound specialization in the presence of computational effectsPublished by Springer Nature ,1997
- A Naïve Time Analysis and its Theory of Cost EquivalenceJournal of Logic and Computation, 1995
- Parallel Reductions in λ-CalculusInformation and Computation, 1995
- M-LISP: a representation-independent dialect of LISP with reduction semanticsACM Transactions on Programming Languages and Systems, 1992
- Notions of computation and monadsInformation and Computation, 1991
- On abstraction and the expressive power of programming languagesPublished by Springer Nature ,1991
- Call-by-name, call-by-value and the λ-calculusTheoretical Computer Science, 1975