| 1. |
- Calcagno, Cristiano, et al.
(författare)
-
Closed Types as a Simple Approach to Safe Imperative Multi-Stage Programming
- 2000
-
Ingår i: Automata, Languages and Programming. - Heidelberg : Springer. - 9783540677154 - 9783540450221 ; , s. 25-36
-
Konferensbidrag (refereegranskat)abstract
- Safely adding computational effects to a multi-stage language has been an open problem. In previous work, a closed type constructor was used to provide a safe mechanism for executing dynamically generated code. This paper proposes a general notion of closed type as a simple approach to safely introducing computational effects into multi-stage languages. We demonstrate this approach formally in a core language called Mini-MLref BN. This core language combines safely multi-stage constructs and ML-style references. In addition to incorporating state, Mini-ML ref BN also embodies a number of technical improvements over previously proposed core languages for multi-stage programming.
|
|
| 2. |
- Calcagno, Cristiano, et al.
(författare)
-
Implementing Multi-stage Languages Using ASTs, Gensym, and Reflection
- 2003
-
Ingår i: Generative Programming and Component Engineering. - Heidelberg : Springer Berlin/Heidelberg. - 9783540201021 - 9783540398158 ; , s. 57-76
-
Konferensbidrag (refereegranskat)abstract
- The paper addresses theoretical and practical aspects of implementing multi-stage languages using abstract syntax trees (ASTs), gensym, and reflection. We present an operational account of the correctness of this approach, and report on our experience with a bytecode compiler called MetaOCaml that is based on this strategy. Current performance measurements reveal interesting characteristics of the underlying OCaml compiler, and illustrate why this strategy can be particularly useful for implementing domain-specific languages in a typed, functional setting. © Springer-Verlag Berlin Heidelberg 2003.
|
|
| 3. |
- Calcagno, Cristiano, et al.
(författare)
-
ML-like Inference for Classifiers
- 2004
-
Ingår i: Programming Languages and Systems. - Heidelberg : Springer Berlin/Heidelberg. - 9783540213130 - 9783540247258 ; , s. 79-93
-
Konferensbidrag (refereegranskat)abstract
- Environment classifiers were proposed as a new approach to typing multi-stage languages. Safety was established in the simply-typed and let-polymorphic settings. While the motivation for classifiers was the feasibility of inference, this was in fact not established. This paper starts with the observation that inference for the full classifier-based system fails. We then identify a subset of the original system for which inference is possible. This subset, which uses implicit classifiers, retains significant expressivity (e.g. it can embed the calculi of Davies and Pfenning) and eliminates the need for classifier names in terms. Implicit classifiers were implemented in MetaOCaml, and no changes were needed to make an existing test suite acceptable by the new type checker. © Springer-Verlag 2004.
|
|
| 4. |
- Czarnecki, Krzysztof, et al.
(författare)
-
DSL Implementation in MetaOCaml, Template Haskell, and C+
- 2004
-
Ingår i: Domain-Specific Program Generation. - Berlin : Springer Berlin/Heidelberg. - 9783540221197 - 9783540259350 ; , s. 51-72
-
Konferensbidrag (refereegranskat)abstract
- A wide range of domain-specific languages (DSLs) has been implemented successfully by embedding them in general purpose languages. This paper reviews embedding, and summarizes how two alternative techniques - staged interpreters and templates - can be used to overcome the limitations of embedding. Both techniques involve a form of generative programming. The paper reviews and compares three programming languages that have special support for generative programming. Two of these languages (MetaOCaml and Template Haskell) are research languages, while the third (C++) is already in wide industrial use. The paper identifies several dimensions that can serve as a basis for comparing generative languages.
|
|
| 5. |
- Ganz, Steven E., et al.
(författare)
-
Macros as Multi-Stage Computations : Type-Safe, Generative, Binding Macros in MacroML
- 2001
-
Ingår i: Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming (ICFP'01). - New York, N.Y. : ACM Press. - 1581134150 ; , s. 74-85
-
Konferensbidrag (refereegranskat)abstract
- With few exceptions, macros have traditionally been viewed as operations on syntax trees or even on plain strings. This view makes macros seem ad hoc, and is at odds with two desirable features of contemporary typed functional languages: static typing and static scoping. At a deeper level, there is a need for a simple, usable semantics for macros. This paper argues that these problems can be addressed by formally viewing macros as multi-stage computations. This view eliminates the need for freshness conditions and tests on variable names, and provides a compositional interpretation that can serve as a basis for designing a sound type system for languages supporting macros, or even for compilation. To illustrate our approach, we develop and present MacroML, an extension of ML that supports inlining, recursive macros, and the definition of new binding constructs. The latter is subtle, and is the most novel addition in a statically typed setting. The semantics of a core subset of MacroML is given by an interpretation into MetaML, a statically-typed multi-stage programming language. It is then easy to show that MacroML is stage- and type-safe: macro expansion does not depend on runtime evaluation, and both stages do not "go wrong.
|
|
| 6. |
- Kiselyov, Oleg, et al.
(författare)
-
A Methodology for Generating Verified Combinatorial Circuits
- 2004
-
Ingår i: EMSOFT '04. - New York, NY : ACM Press. - 1581138601 ; , s. 249-258
-
Konferensbidrag (refereegranskat)abstract
- High-level programming languages offer significant expressivity but provide little or no guarantees about resource use. Resource-bounded languages --- such as hardware-description languages --- provide strong guarantees about the runtime behavior of computations but often lack mechanisms that allow programmers to write more structured, modular, and reusable programs. To overcome this basic tension in language design, recent work advocated the use of Resource-aware Programming (RAP) languages, which take into account the natural distinction between the development platform and the deployment platform for resource-constrained software.This paper investigates the use of RAP languages for the generation of combinatorial circuits. The key challenge that we encounter is that the RAP approach does not safely admit a mechanism to express a posteriori (post-generation) optimizations. The paper proposes and studies the use of abstract interpretation to overcome this problem. The approach is illustrated using an in-depth analysis of the Fast Fourier Transform (FFT). The generated computations are comparable to those generated by FFTW.
|
|
| 7. |
- Kiselyov, Oleg, et al.
(författare)
-
Relating FFTW and Split-Radix
- 2004
-
Ingår i: Embedded Software and Systems. - Berlin : Springer Berlin/Heidelberg. - 9783540281283 - 9783540318231 ; , s. 488-493
-
Konferensbidrag (refereegranskat)abstract
- Recent work showed that staging and abstract interpretation can be used to derive correct families of combinatorial circuits, and illustrated this technique with an in-depth analysis of the Fast Fourier Transform (FFT) for sizes 2n. While the quality of the generated code was promising, it used more floating-point operations than the well-known FFTW codelets and split-radix algorithm. This paper shows that staging and abstract interpretation can in fact be used to produce circuits with the same number of floating-point operations as each of split-radix and FFTW. In addition, choosing between two standard implementations of complex multiplication produces results that match each of the two algorithms. Thus, we provide a constructive method for deriving the two distinct algorithms. © Springer-Verlag Berlin Heidelberg 2005.
|
|
| 8. |
- Ostrovsky, Karol, 1975, et al.
(författare)
-
Towards a Primitive Higher Order Calculus of Broadcasting Systems
- 2002
-
Ingår i: PPDP '02. - New York, NY : ACM Press. - 1581135289 ; , s. 2-13
-
Konferensbidrag (refereegranskat)abstract
- Ethernet-style broadcast is a pervasive style of computer communication. In this style, the medium is a single nameless channel. Previous work on modelling such systems proposed a first order process calculus called CBS. In this paper, we propose a fundamentally different calculus called HOBS. Compared to CBS, HOBS 1) is higher order rather than first order, 2) supports dynamic subsystem encapsulation rather than static, and 3) does not require an "underlying language" to be Turing-complete. Moving to a higher order calculus is key to increasing the expressivity of the primitive calculus and alleviating the need for an underlying language. The move, however, raises the need for significantly more machinery to establish the basic properties of the new calculus. This paper develops the basic theory for HOBS and presents two example programs that illustrate programming in this language. The key technical underpinning is an adaptation of Howe's method to HOBS to prove that bisimulation is a congruence. From this result, HOBS is shown to embed the lazy λ-calculus.
|
|
| 9. |
- Pašalić, Emir, et al.
(författare)
-
Tagless Staged Interpreters for Typed Languages
- 2002
-
Ingår i: ICFP '02. - New York, NY : ACM Press. - 1581134878 ; , s. 218-229
-
Konferensbidrag (refereegranskat)abstract
- Multi-stage programming languages provide a convenient notation for explicitly staging programs. Staging a definitional interpreter for a domain specific language is one way of deriving an implementation that is both readable and efficient. In an untyped setting, staging an interpreter "removes a complete layer of interpretive overhead", just like partial evaluation. In a typed setting however, Hindley-Milner type systems do not allow us to exploit typing information in the language being interpreted. In practice, this can mean a slowdown cost by a factor of three or more. Previously, both type specialization and tag elimination were applied to this problem. In this paper we propose an alternative approach, namely, expressing the definitional interpreter in a dependently typed programming language. We report on our experience with the issues that arise in writing such an interpreter and in designing such a language. To demonstrate the soundness of combining staging and dependent types in a general sense, we formalize our language (called Meta-D) and prove its type safety. To formalize Meta-D, we extend Shao, Saha, Trifonov and Papaspyrou's λH language to a multilevel setting. Building on λH allows us to demonstrate type safety in a setting where the type language contains all the calculus of inductive constructions, but without having to repeat the work needed for establishing the soundness of that system.
|
|
| 10. |
-
Semantics, applications, and implementation of program generation : second international workshop, SAIG 2001, Florence, Italy, September 6, 2001 00 : proceedings
- 2001
-
Proceedings (redaktörskap) (övrigt vetenskapligt/konstnärligt)abstract
- This book constitutes the refereed proceedings of the Second International Workshop on Semantics, Applications, and Implementation of Program Generation, SAIG 2001, held in Florence, Italy in September 2001. The seven revised full papers and two position papers presented together with an invited survey paper and two abstracts of invited talks were carefully reviewed and selected for inclusion in the book. Among the topics covered are generative programming, meta-programming, aspect-oriented programming, transition compression, goal-directed evaluation, partial evaluation, functional programming, meta-computation, and program optimization.
|
|
