| 1. |
- Benaissa, Zine El-Abidine, et al.
(författare)
-
Logical Modalities and Multi-Stage Programming
- 1999
-
Konferensbidrag (refereegranskat)abstract
- Multi-stage programming is a method for improving the performance of programs through the introduction of controlled program specialization. This paper makes a case for multi-stage programming with open code and closed values. We argue that a simple language exploiting interactions between two logical modalities is well suited for multi-stage programming, and report the results from our study of categorical models for multi-stage languages.
|
|
| 2. |
- Moggi, Eugenio, et al.
(författare)
-
An Idealized MetaML : Simpler, and More Expressive
- 1999
-
Ingår i: Programming Languages and Systems. - Berlin : Springer Berlin/Heidelberg. - 3540656995 ; , s. 193-207
-
Konferensbidrag (refereegranskat)abstract
- MetaML is a multi-stage functional programming language featuring three constructs that can be viewed as statically-typed refinements of the back-quote, comma, and eval of Scheme. Thus it provides special support for writing code generators and serves as a semanticallysound basis for systems involving multiple interdependent computational stages. In previous work, we reported on an implementation of MetaML, and on a reduction semantics and type-system for MetaML. In this paper, we present An Idealized MetaML (AIM) that is the result of our study of a categorical model for MetaML. An important outstanding problem is finding a type system that provides the user with a means for manipulating both open and closed code. This problem has eluded efforts by us and other researchers for over three years. AIM solves the issue by providing two type constructors, one classifies closed code and the other open code, and exploiting the way they interact. We point out that AIM can be verbose, and outline a possible remedy relating to the strictness of the closed code type. © Springer International Publishing AG, Part of Springer Science+Business Media 1999
|
|
| 3. |
- Taha, Walid, 1971-, et al.
(författare)
-
Multi-Stage Programming : Axiomatization and Type-Safety
- 1998
-
Ingår i: Automata, Languages and Programming. - Berlin : Springer Berlin/Heidelberg. - 9783540647812 - 9783540686811 ; , s. 918-929
-
Konferensbidrag (refereegranskat)abstract
- Multi-stage programming provides a new paradigm for constructing efficient solutions to complex problems. Techniques such as program generation, multi-level partial evaluation, and run-time code generation respond to the need for general purpose solutions which do not pay run-time interpretive overheads. This paper provides a foundation for the formal analysis of one such system.We introduce a multi-stage language and present its axiomatic and reduction semantics. Our axiomatic semantics is an extension of the call-by-value λ-calculus with staging constructs. We show that staged-languages can “go Wrong” in new ways, and devise a type system that screens out such programs. Finally, we present a proof of the soundness of this type system with respect to the reduction semantics. © Springer 1998
|
|
| 4. |
- Taha, Walid, 1971-
(författare)
-
Multi-Stage Programming : Its Theory and Applications
- 1999
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- MetaML is a statically typed functional programming language with special support for programgeneration. In addition to providing the standard features of contemporary programminglanguages such as Standard ML, MetaML provides three staging annotations. These staging annotationsallow the construction, combination, and execution of object-programs.Our thesis is that MetaML's three staging annotations provide a useful, theoretically soundbasis for building program generators. This dissertation reports on our study of MetaML's stagingconstructs, their use, their implementation, and their formal semantics. Our results include anextended example of where MetaML allows us to produce ecient programs, an explanation ofwhy implementing these constructs in traditional ways can be challenging, two formulations ofMetaML's semantics, a type system for MetaML, and a proposal for extending MetaML with atype construct for closedness.The dissertation consolidates a number of previous publications by the author, includingMetaML's type systems and big-step semantics. The presentation is new. The proposed solutionto an implementation problem and the reduction semantics for MetaML's three staging constructsare also new.
|
|
| 5. |
- Taha, Walid, 1971-, et al.
(författare)
-
Multi-Stage Programming with Explicit Annotations
- 1997
-
Ingår i: PEPM '97. - New York, NY : ACM Press. - 0897919173 ; , s. 203-217
-
Konferensbidrag (refereegranskat)abstract
- We introduce MetaML, a statically-typed multi-stage programming language extending Nielson and Nielson's two stage notation to an arbitrary number of stages. MetaML extends previous work by introducing four distinct staging annotations which generalize those published previously [25, 12, 7, 6]. We give a static semantics in which type checking is done once and for all before the first stage, and a dynamic semantics which introduces a new concept of cross-stage persistence, which requires that variables available in any stage are also available in all future stages. We illustrate that staging is a manual form of binding time analysis. We explain why, even in the presence of automatic binding time analysis, explicit annotations are useful, especially for programs with more than two stages. A thesis of this paper is that multi-stage languages are useful as programming languages in their own right, and should support features that make it possible for programmers to write staged computations without significantly changing their normal programming style. To illustrate this we provide a simple three stage example, and an extended two-stage example elaborating a number of practical issues.
|
|
| 6. |
|
|
