SK
S. Keidel
info
Please Note
<p>This page displays the records of the person named above and is not linked to a unique person identifier. This record may need to be merged to a profile.</p>
3 records found
1
Abstract interpretation is a technique for developing static analyses. Yet, proving abstract interpreters sound is challenging for interesting analyses, because of the high proof complexity and proof effort. To reduce complexity and effort, we propose a framework for abstract interpreters that makes their soundness proof compositional. Key to our approach is to capture the similarities between concrete and abstract interpreters in a single shared interpreter, parameterized over an arrow-based interface. In our framework, a soundness proof is reduced to proving reusable soundness lemmas over the concrete and abstract instances of this interface; the soundness of the overall interpreters follows from a generic theorem. To further reduce proof effort, we explore the relationship between soundness and parametricity. Parametricity not only provides us with useful guidelines for how to design non-leaky interfaces for shared interpreters, but also provides us soundness of shared pure functions as free theorems. We implemented our framework in Haskell and developed a k-CFA analysis for PCF and a tree-shape analysis for Stratego. We were able to prove both analyses sound compositionally with manageable complexity and effort, compared to a conventional soundness proof.
...
Abstract interpretation is a technique for developing static analyses. Yet, proving abstract interpreters sound is challenging for interesting analyses, because of the high proof complexity and proof effort. To reduce complexity and effort, we propose a framework for abstract interpreters that makes their soundness proof compositional. Key to our approach is to capture the similarities between concrete and abstract interpreters in a single shared interpreter, parameterized over an arrow-based interface. In our framework, a soundness proof is reduced to proving reusable soundness lemmas over the concrete and abstract instances of this interface; the soundness of the overall interpreters follows from a generic theorem. To further reduce proof effort, we explore the relationship between soundness and parametricity. Parametricity not only provides us with useful guidelines for how to design non-leaky interfaces for shared interpreters, but also provides us soundness of shared pure functions as free theorems. We implemented our framework in Haskell and developed a k-CFA analysis for PCF and a tree-shape analysis for Stratego. We were able to prove both analyses sound compositionally with manageable complexity and effort, compared to a conventional soundness proof.
Developers of program transformations often reason about transformations to assert certain properties of the generated
code. We propose to apply abstract interpretation to program transformations in order to automate and support such
reasoning. In this paper, we present work in progress on the development and application of an abstract interpreter for
the program transformation language Stratego. In particular, we present challenges encountered during the development
of the abstract Stratego interpreter and how we intend to solve these challenges.
...
Developers of program transformations often reason about transformations to assert certain properties of the generated
code. We propose to apply abstract interpretation to program transformations in order to automate and support such
reasoning. In this paper, we present work in progress on the development and application of an abstract interpreter for
the program transformation language Stratego. In particular, we present challenges encountered during the development
of the abstract Stratego interpreter and how we intend to solve these challenges.
Modern IDEs support multiple programming languages via plug-ins, but developing a high-quality language plug-in is a huge development effort and individual plug-ins are not reusable in other IDEs. We call this the IDE portability problem.
In this paper, we present a solution to the IDE portability problem based on a language-independent and IDE-independent intermediate representation (IR) for editor-service products. This IR enables IDE-independent language services to provide editor services for arbitrary IDEs, using language-independent IDE plug-ins.
We combine the IR with a service-oriented architecture to facilitate the modular addition of language services, the decomposition of language services into smaller interdependent services, and the use of arbitrary implementation languages for services.
To evaluate the feasibility of our design, we have implemented the IR and architecture in a framework called Monto. We demonstrate the generality of our design by constructing language services for Java, JavaScript, Python, and Haskell and show that they are reusable in the Eclipse IDE and in a web-based IDE. We also evaluate the performance of Monto and show that Monto is responsive and has admissible performance overhead.
...
In this paper, we present a solution to the IDE portability problem based on a language-independent and IDE-independent intermediate representation (IR) for editor-service products. This IR enables IDE-independent language services to provide editor services for arbitrary IDEs, using language-independent IDE plug-ins.
We combine the IR with a service-oriented architecture to facilitate the modular addition of language services, the decomposition of language services into smaller interdependent services, and the use of arbitrary implementation languages for services.
To evaluate the feasibility of our design, we have implemented the IR and architecture in a framework called Monto. We demonstrate the generality of our design by constructing language services for Java, JavaScript, Python, and Haskell and show that they are reusable in the Eclipse IDE and in a web-based IDE. We also evaluate the performance of Monto and show that Monto is responsive and has admissible performance overhead.
...
Modern IDEs support multiple programming languages via plug-ins, but developing a high-quality language plug-in is a huge development effort and individual plug-ins are not reusable in other IDEs. We call this the IDE portability problem.
In this paper, we present a solution to the IDE portability problem based on a language-independent and IDE-independent intermediate representation (IR) for editor-service products. This IR enables IDE-independent language services to provide editor services for arbitrary IDEs, using language-independent IDE plug-ins.
We combine the IR with a service-oriented architecture to facilitate the modular addition of language services, the decomposition of language services into smaller interdependent services, and the use of arbitrary implementation languages for services.
To evaluate the feasibility of our design, we have implemented the IR and architecture in a framework called Monto. We demonstrate the generality of our design by constructing language services for Java, JavaScript, Python, and Haskell and show that they are reusable in the Eclipse IDE and in a web-based IDE. We also evaluate the performance of Monto and show that Monto is responsive and has admissible performance overhead.
In this paper, we present a solution to the IDE portability problem based on a language-independent and IDE-independent intermediate representation (IR) for editor-service products. This IR enables IDE-independent language services to provide editor services for arbitrary IDEs, using language-independent IDE plug-ins.
We combine the IR with a service-oriented architecture to facilitate the modular addition of language services, the decomposition of language services into smaller interdependent services, and the use of arbitrary implementation languages for services.
To evaluate the feasibility of our design, we have implemented the IR and architecture in a framework called Monto. We demonstrate the generality of our design by constructing language services for Java, JavaScript, Python, and Haskell and show that they are reusable in the Eclipse IDE and in a web-based IDE. We also evaluate the performance of Monto and show that Monto is responsive and has admissible performance overhead.