PEPM 2023 – Proceedings

Message from the Chairs
We are pleased to present the proceedings of the 2023 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2023), held January 16-17th, 2023 in Boston, in affiliation with the annual Symposium on Principles of Programming Languages (POPL 2023).
PEPM has a history going back to 1991 and originated with the discoveries of 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 subjects to black-box execution but also as data structures that can be generated, analysed, and transformed while establishing or maintaining important semantic properties.

Papers

Semantic Transformation Framework for Rewriting Rules
Jihee Park, Jaemin Hong, and Sukyoung Ryu
(KAIST, South Korea)
Semantics-preserving source-to-source program transformations, such as optimization and refactoring, are essential for software development. Such transformations are often defined by rewriting rules describing which part of a program must be replaced with which subprogram. The main obstacle to designing a transformation is to prove its semantics preservation. Rewriting-rule-based frameworks alleviate this difficulty by giving proof guidelines or automating the proofs. Unfortunately, each framework is applicable to a restricted set of transformations due to a fixed definition of semantics preservation. Cousot and Cousot’s semantic transformation framework resolves this problem by leaving a space for its users to define a proper semantics preservation property. However, the framework does not exploit the characteristic of rewriting rules and fails to ease the proofs. In this work, we define a semantic transformation framework tailored to rewriting rules by refining Cousot and Cousot’s framework. Our framework facilitates modular proofs by providing syntax-directed guidelines and theorems that simplify proofs. We show the versatility of our framework by proving the semantics preservation of six well-known transformations.

Publisher's Version

Symbolic Execution of Hadamard-Toffoli Quantum Circuits
Jacques Carette, Gerardo Ortiz, and Amr Sabry
(McMaster University, Canada; Indiana University, USA)
The simulation of quantum programs by classical computers is a critical endeavor for several reasons: it provides proof-of-concept validation of quantum algorithms; it provides opportunities to experiment with new programming abstractions suitable for the quantum domain; and most significantly it is a way to explore the elusive boundary at which a quantum advantage may materialize. Here, we show that traditional techniques of symbolic evaluation and partial evaluation yield surprisingly efficient classical simulations for some instances of textbook quantum algorithms that include the Deutsch, Deutsch-Jozsa, Bernstein-Vazirani, Simon, Grover, and Shor's algorithms. The success of traditional partial evaluation techniques in this domain is due to one simple insight: the quantum bits used in these algorithms can be modeled by a symbolic boolean variable while still keeping track of the correlations due to superposition and entanglement. More precisely, the system of constraints generated over the symbolic variables contains all the necessary quantum correlations and hence the answer to the quantum algorithms. With a few programming tricks explained in the paper, quantum circuits with millions of gates can be symbolically executed in seconds. Paradoxically, other circuits with as few as a dozen gates take exponential time. We reflect on the significance of these results in the conclusion.

Publisher's Version

Published Artifact

Artifacts Available

Generating Programs for Polynomial Multiplication with Correctness Assurance
Ryo Tokuda and Yukiyoshi Kameyama
(University of Tsukuba, Japan)
Program-generation techniques prevail in domains that need high performance, such as linear algebra, image processing, and database. Yet, it is hard to generate high-performance programs with correctness assurance, and cryptography needs both. Masuda and Kameyama proposed a DSL-based framework for implementing a program generator, an analyzer, and a formula generator, and obtained an efficient and correct implementation of Number-Theoretic Transform (NTT) that is necessary for many cryptographic algorithms.
This paper advances their study in two ways. First, we develop a generation-and-analysis framework so that program generation is driven by program analysis. As a concrete result, we have found an optimization missed in previous studies. Second, we investigate whether the framework can be applied to other algorithms, including inverse NTT. By combining generated programs, we have obtained an efficient and correct implementation of polynomial multiplication, the key for several post-quantum cryptographic algorithms.

Publisher's Version

Efficient Embedding of Strategic Attribute Grammars via Memoization
José Nuno Macedo, Emanuel Rodrigues, Marcos Viera, and João Saraiva
(HASLab - INESC TEC, Portugal; University of Minho, Portugal; Universidad de la República, Uruguay)
Strategic term re-writing and attribute grammars are two powerful programming techniques widely used in language engineering. The former relies on strategies to apply term re-write rules in defining large-scale language transformations, while the latter is suitable to express context-dependent language processing algorithms. These two techniques can be expressed and combined via a powerful navigation abstraction: generic zippers. This results in a concise zipper-based embedding offering the expressiveness of both techniques.
Such elegant embedding has a severe limitation since it recomputes attribute values. This paper presents a proper and efficient embedding of both techniques. First, attribute values are memoized in the zipper data structure, thus avoiding their re-computation. Moreover, strategic zipper based functions are adapted to access such memoized values. We have implemented our memoized embedding as the Ztrategic library and we benchmarked it against the state-of-the-art Strafunski and Kiama libraries. Our first results show that we are competitive against those two well established libraries.

Publisher's Version

Towards a Reflection for Effect Handlers
Youyou Cong and Kenichi Asai
(Tokyo Institute of Technology, Japan; Ochanomizu University, Japan)
A reflection is a relationship between compiling and decompiling functions. This concept has been studied as a means to ensure correctness of compilers, in particular, those for languages featuring control effects. We aim to develop a reflection for algebraic effects and handlers. As a first step towards this goal, we investigate what we obtain by following the existing recipe for control operators. We show that, if we use the simplest CPS translation as the compiling function, we can prove most but not all theorems required of a reflection. From this result, we identify two conditions of the CPS translation that would lead to a reflection for effect handlers.

Publisher's Version

PEPM 2023 – Proceedings

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

Frontmatter

Papers