POPL 2020 Co-Located Events
POPL 2020 Co-Located Events
Powered by
Conference Publishing Consulting

2020 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2020), January 20, 2020, New Orleans, LA, USA

PEPM 2020 – Proceedings

Contents - Abstracts - Authors

2020 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2020)


Title Page

Message from the Chairs
We are pleased to present the proceedings of the 2020 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2020), held in New Orleans, Louisiana, United States, January 20th, 2020, in affiliation with the annual Symposium on Principles of Programming Languages (POPL 2020). PEPM has a history going back to 1991, and originates in the discoveries of practically useful automated techniques for evaluating programs with only partial input. Over the years, the scope of PEPM has expanded to include a variety of research areas centered around the theme of semantics-based program manipulation — the systematic exploitation of treating programs not only as subject to black-box execution, but also as data structures that can be generated, analyzed, and transformed while establishing or maintaining important semantic properties. Relevant topics span from refactoring, partial evaluation, supercompilation, staged programming, fusion, and other meta-programming to model-driven development, program analysis, inductive programming, decompilation, program generation, and abstract interpretation.

Research Papers

Module Generation without Regret
Yuhi Sato, Yukiyoshi Kameyama, and Takahisa Watanabe
(University of Tsukuba, Japan)
Modules are an indispensable mechanism for providing abstraction to programming languages. To reduce the abstraction overhead in the usage of modules, Watanabe et al. proposed a language for generating and manipulating code of modules, and implemented it via a translation to plain MetaOCaml. Unfortunately, their solution has a serious problem of code explosion if functors are repeatedly applied to modules. Another problem in their solution is that it does not allow nested modules.
This paper proposes a refined translation for a two-stage typed language with module generation where nested modules are allowed. Our translation does not suffer from the code-duplication problem. The key idea is to use the genlet operator in latest MetaOCaml, which performs let insertion at the code-generation time to allow sharing of code fragments. To our knowledge, our work is the first to apply genlet to code generation for modules. We conduct an experiment using a microbenchmark, and the result shows that our method is effective to reduce the size of generated code that would have been exponentially large.

Publisher's Version Article Search
Symbolic Bisimulation for Open and Parameterized Systems
Zechen Hou and Eric Madelaine
(East China Normal University, China; Inria, France)
Open Automata (OA) are symbolic and parameterized models for open concurrent systems. Here open means partially specified systems, that can be instantiated or assembled to build bigger systems. An important property for such systems is ”compositionality”, meaning that logical properties, and equivalences, can be checked locally, and will be preserved by composition. In previous work, a notion of equivalence named FH-Bisimulation was defined for open-automata, and proved to be a congruence for their composition. But this equivalence was defined for a variant of open-automata that are intrinsically infinite, making it unsuitable for algorithmic treatment.
We define a new form of equivalence named StrFH-Bisimulation, working on finite encodings of OAs. We prove that StrFH-Bisimulation is consistent and complete with respect to the FH-Bisimulation.
Then we propose two algorithms to check StrFH-Bisimulation: the first one requires a (user-defined) relation between the states of two finite OAs, and checks whether it is a StrFH-Bisimulation. The second one takes two finite OAs as input, and builds a ”weakest StrFH-bisimulation” such that their initial states are bisimilar. We prove that this algorithm terminates when the data domains are finite. Both algorithms use an SMT-solver as a basis to solve the proof obligations.

Publisher's Version Article Search
High-Fidelity Metaprogramming with Separator Syntax Trees
Rodin T. A. Aarssen and Tijs van der Storm
(CWI, Netherlands; Eindhoven University of Technology, Netherlands; University of Groningen, Netherlands)
Many metaprogramming tasks, such as refactorings, automated bug fixing, or large-scale software renovation, require high-fidelity source code transformations -- transformations which preserve comments and layout as much as possible. Abstract syntax trees (ASTs) typically abstract from such details, and hence would require pretty printing, destroying the original program layout. Concrete syntax trees (CSTs) preserve all layout information, but transformation systems or parsers that support CSTs are rare and can be cumbersome to use.
In this paper we present separator syntax trees (SSTs), a lightweight syntax tree format, that sits between AST and CSTs, in terms of the amount of information they preserve. SSTs extend ASTs by recording textual layout information separating AST nodes. This information can be used to reconstruct the textual code after parsing, but can largely be ignored when implementing high-fidelity transformations.
We have implemented SSTs in Rascal, and show how it enables the concise definition of high-fidelity source code transformations using a simple refactoring for C++.

Publisher's Version Article Search

Short Papers

An Approach to Generate Text-Based IDEs for Syntax Completion Based on Syntax Specification
Isao Sasano
(Shibaura Institute of Technology, Japan)
The integrated development environments provide several types of functionalities. Herein, we intend to generate a syntax completion functionality from the grammar of the target language as long as the sentences of the language can be analyzed via LR parsing. We specify the syntax candidates to be completed based on the sentential forms and reductions in LR parsing. Furthermore, we implement a prototype system for computing the syntax candidates to be completed at the cursor position in the source code written in a small subset of Standard ML; the system only uses the program text up to the cursor position to ensure simplicity.

Publisher's Version Article Search
GOOL: A Generic Object-Oriented Language
Jacques Carette, Brooks MacLachlan, and Spencer Smith
(McMaster University, Canada)
We present GOOL, a Generic Object-Oriented Language. GOOL shows that with the right abstractions, a language can capture the essence of object-oriented programs. GOOL generates human-readable, documented and idiomatic code in Python, Java, C#, and C++. In it, we can express common programming idioms and patterns.

Publisher's Version Article Search

proc time: 4.16