The proceedings contains nine papers from the Proceedings of the 2003 acmsigplanworkshop on partialevaluation and semantics-basedprogrammanipulation (PEPM'03). Topics discussed include: fast partial evaluatio...
详细信息
The proceedings contains nine papers from the Proceedings of the 2003 acmsigplanworkshop on partialevaluation and semantics-basedprogrammanipulation (PEPM'03). Topics discussed include: fast partialevaluation of pattern matching in strings;transforming interpreters into inverse interpreters by partialevaluation;implementing typeful programs transformations;abstract specialization and its applications;slicing Java programs that throw and catch exceptions;storeless semantics and alias logic;and extending sized type with collection analysis.
In this paper we study the connection between the structure of relational abstract domains for program analysis and compositionality of the underlying semantics. Both can be systematically designed as solution of the ...
详细信息
In this paper we study the connection between the structure of relational abstract domains for program analysis and compositionality of the underlying semantics. Both can be systematically designed as solution of the same abstract domain equation involving the same domain refinement: the reduced power operation. We prove that most well-known compositional semantics of imperative programs, such as the standard denotational and weakest precondition semantics can be systematically derived as solutions of simple abstract domain equations. This provides an equational presentation of both semantics and abstract domains for program analysis in a unique formal setting. Moreover both finite and transfinite compositional semantics share the same structure, and this allows us to provide consistent models for programmanipulation.
partialevaluation is a program-transformation technique that automatically specializes a program with respect to user-supplied invariants. Despite successful applications in areas such as graphics, operating systems,...
详细信息
partialevaluation is a program-transformation technique that automatically specializes a program with respect to user-supplied invariants. Despite successful applications in areas such as graphics, operating systems, and software engineering, partial evaluators have yet to achieve widespread use. One reason is the difficulty of adequately describing specialization opportunities. Indeed, under-specialization or over-specialization often occurs, without any direct feedback to the user as to the source of the problem. We have developed a high-level, module-based language allowing the programmer to guide the choice of both the code to specialize and the invariants to exploit during the specialization process. To ease the use of partialevaluation, the syntax of this language is similar to the declaration syntax of the target language of the partial evaluator. To provide feedback to the programmer, declarations are checked throughout the analyses performed by partialevaluation. The language has been successfully used by a signal-processing expert in the design of a specializable Forward Error Correction component.
We define an operational semantics for a large part of the Android platform, encompassing the Dalvik bytecode but also, and more importantly, the inter-component communication mechanism used inside Android application...
详细信息
ISBN:
(纸本)9781450326193
We define an operational semantics for a large part of the Android platform, encompassing the Dalvik bytecode but also, and more importantly, the inter-component communication mechanism used inside Android applications. This semantics is intended to provide a formal basis for the development of static analyses that consider the complex flow of information exposed by the cooperating components of Android applications.
This paper presents an online partial evaluator for the lambda-calculus with the delimited continuation constructs shift and reset. We first give the semantics of the delimited continuation constructs in two ways: one...
详细信息
ISBN:
(纸本)9781581134551
This paper presents an online partial evaluator for the lambda-calculus with the delimited continuation constructs shift and reset. We first give the semantics of the delimited continuation constructs in two ways: one by writing a continuation passing style (CPS) interpreter and the other by transforming them into CPS. We then combine them to obtain a partial evaluator written in CPS which produces the result in CPS. By transforming this partial evaluator back into a direct style (DS) in two steps, we obtain a DS to DS partial evaluator written in DS. The correctness of the partial evaluator is not yet formally proven. The difficulty comes from the fact that the partial evaluator is written using shift and reset. The method for reasoning about such programs is not yet established. However, the development of the partial evaluator is detailed in the paper to give a degree of confidence that it behaves as we expect.
Any expression M in ULC (the untyped A lambda-calculus) can be compiled into a rather low-level language we call LLL, whose programs contain none of the traditional implementation devices for functional languages: env...
详细信息
ISBN:
(纸本)9781450347211
Any expression M in ULC (the untyped A lambda-calculus) can be compiled into a rather low-level language we call LLL, whose programs contain none of the traditional implementation devices for functional languages: environments, thunks, closures, etc. A compiled program is first-order functional and has a fixed set of working variables, whose number is independent of M. The generated LLL code in effect traverses the subexpressions of M. We apply the techniques of game semantics to the untyped A calculus, but take a more operational viewpoint that uses less mathematical machinery than traditional presentations of game semantics. Further, the untyped lambda calculus ULC is compiled into LLL by partially evaluating a traversal algorithm for ULC.
The aim of many program transformers is to improve efficiency while preserving program meaning. Correctness issues have been dealt with extensively. However, very little attention has been paid to formally establish t...
详细信息
ISBN:
(纸本)9781581134551
The aim of many program transformers is to improve efficiency while preserving program meaning. Correctness issues have been dealt with extensively. However, very little attention has been paid to formally establish the improvements achieved by these transformers. In this work, we introduce the scheme of a narrowing-driven partial evaluator enhanced with abstract costs. They are "abstract" in the sense that they measure the number of basic operations performed during a computation rather than actual execution times. Thus, we have available a setting in which one can discuss the effects of the program transformer in a precise framework and, moreover, to quantify these effects. Our scheme may serve as a basis to develop speedup analyses and cost-guided transformers. An implementation of the cost-augmented specializer has been undertaken, which demonstrates the practicality of our approach.
暂无评论