Workshop PEPM 2023 – Author Index 
Contents 
Abstracts 
Authors

Asai, Kenichi 
PEPM '23: "Towards a Reflection for Effect ..."
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. @InProceedings{PEPM23p55, author = {Youyou Cong and Kenichi Asai}, title = {Towards a Reflection for Effect Handlers}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {5565}, doi = {10.1145/3571786.3573015}, year = {2023}, } Publisher's Version 

Carette, Jacques 
PEPM '23: "Symbolic Execution of HadamardToffoli ..."
Symbolic Execution of HadamardToffoli 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 proofofconcept 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, DeutschJozsa, BernsteinVazirani, 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. @InProceedings{PEPM23p14, author = {Jacques Carette and Gerardo Ortiz and Amr Sabry}, title = {Symbolic Execution of HadamardToffoli Quantum Circuits}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {1426}, doi = {10.1145/3571786.3573018}, year = {2023}, } Publisher's Version Published Artifact Artifacts Available 

Cong, Youyou 
PEPM '23: "Towards a Reflection for Effect ..."
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. @InProceedings{PEPM23p55, author = {Youyou Cong and Kenichi Asai}, title = {Towards a Reflection for Effect Handlers}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {5565}, doi = {10.1145/3571786.3573015}, year = {2023}, } Publisher's Version 

Hong, Jaemin 
PEPM '23: "Semantic Transformation Framework ..."
Semantic Transformation Framework for Rewriting Rules
Jihee Park , Jaemin Hong , and Sukyoung Ryu (KAIST, South Korea) Semanticspreserving sourcetosource 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. Rewritingrulebased 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 syntaxdirected guidelines and theorems that simplify proofs. We show the versatility of our framework by proving the semantics preservation of six wellknown transformations. @InProceedings{PEPM23p1, author = {Jihee Park and Jaemin Hong and Sukyoung Ryu}, title = {Semantic Transformation Framework for Rewriting Rules}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {113}, doi = {10.1145/3571786.3573016}, year = {2023}, } Publisher's Version 

Kameyama, Yukiyoshi 
PEPM '23: "Generating Programs for Polynomial ..."
Generating Programs for Polynomial Multiplication with Correctness Assurance
Ryo Tokuda and Yukiyoshi Kameyama (University of Tsukuba, Japan) Programgeneration techniques prevail in domains that need high performance, such as linear algebra, image processing, and database. Yet, it is hard to generate highperformance programs with correctness assurance, and cryptography needs both. Masuda and Kameyama proposed a DSLbased framework for implementing a program generator, an analyzer, and a formula generator, and obtained an efficient and correct implementation of NumberTheoretic Transform (NTT) that is necessary for many cryptographic algorithms. This paper advances their study in two ways. First, we develop a generationandanalysis 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 postquantum cryptographic algorithms. @InProceedings{PEPM23p27, author = {Ryo Tokuda and Yukiyoshi Kameyama}, title = {Generating Programs for Polynomial Multiplication with Correctness Assurance}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {2740}, doi = {10.1145/3571786.3573017}, year = {2023}, } Publisher's Version 

Macedo, José Nuno 
PEPM '23: "Efficient Embedding of Strategic ..."
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 rewriting and attribute grammars are two powerful programming techniques widely used in language engineering. The former relies on strategies to apply term rewrite rules in defining largescale language transformations, while the latter is suitable to express contextdependent language processing algorithms. These two techniques can be expressed and combined via a powerful navigation abstraction: generic zippers. This results in a concise zipperbased 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 recomputation. 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 stateoftheart Strafunski and Kiama libraries. Our first results show that we are competitive against those two well established libraries. @InProceedings{PEPM23p41, author = {José Nuno Macedo and Emanuel Rodrigues and Marcos Viera and João Saraiva}, title = {Efficient Embedding of Strategic Attribute Grammars via Memoization}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {4154}, doi = {10.1145/3571786.3573019}, year = {2023}, } Publisher's Version 

Ortiz, Gerardo 
PEPM '23: "Symbolic Execution of HadamardToffoli ..."
Symbolic Execution of HadamardToffoli 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 proofofconcept 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, DeutschJozsa, BernsteinVazirani, 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. @InProceedings{PEPM23p14, author = {Jacques Carette and Gerardo Ortiz and Amr Sabry}, title = {Symbolic Execution of HadamardToffoli Quantum Circuits}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {1426}, doi = {10.1145/3571786.3573018}, year = {2023}, } Publisher's Version Published Artifact Artifacts Available 

Park, Jihee 
PEPM '23: "Semantic Transformation Framework ..."
Semantic Transformation Framework for Rewriting Rules
Jihee Park , Jaemin Hong , and Sukyoung Ryu (KAIST, South Korea) Semanticspreserving sourcetosource 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. Rewritingrulebased 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 syntaxdirected guidelines and theorems that simplify proofs. We show the versatility of our framework by proving the semantics preservation of six wellknown transformations. @InProceedings{PEPM23p1, author = {Jihee Park and Jaemin Hong and Sukyoung Ryu}, title = {Semantic Transformation Framework for Rewriting Rules}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {113}, doi = {10.1145/3571786.3573016}, year = {2023}, } Publisher's Version 

Rodrigues, Emanuel 
PEPM '23: "Efficient Embedding of Strategic ..."
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 rewriting and attribute grammars are two powerful programming techniques widely used in language engineering. The former relies on strategies to apply term rewrite rules in defining largescale language transformations, while the latter is suitable to express contextdependent language processing algorithms. These two techniques can be expressed and combined via a powerful navigation abstraction: generic zippers. This results in a concise zipperbased 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 recomputation. 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 stateoftheart Strafunski and Kiama libraries. Our first results show that we are competitive against those two well established libraries. @InProceedings{PEPM23p41, author = {José Nuno Macedo and Emanuel Rodrigues and Marcos Viera and João Saraiva}, title = {Efficient Embedding of Strategic Attribute Grammars via Memoization}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {4154}, doi = {10.1145/3571786.3573019}, year = {2023}, } Publisher's Version 

Ryu, Sukyoung 
PEPM '23: "Semantic Transformation Framework ..."
Semantic Transformation Framework for Rewriting Rules
Jihee Park , Jaemin Hong , and Sukyoung Ryu (KAIST, South Korea) Semanticspreserving sourcetosource 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. Rewritingrulebased 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 syntaxdirected guidelines and theorems that simplify proofs. We show the versatility of our framework by proving the semantics preservation of six wellknown transformations. @InProceedings{PEPM23p1, author = {Jihee Park and Jaemin Hong and Sukyoung Ryu}, title = {Semantic Transformation Framework for Rewriting Rules}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {113}, doi = {10.1145/3571786.3573016}, year = {2023}, } Publisher's Version 

Sabry, Amr 
PEPM '23: "Symbolic Execution of HadamardToffoli ..."
Symbolic Execution of HadamardToffoli 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 proofofconcept 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, DeutschJozsa, BernsteinVazirani, 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. @InProceedings{PEPM23p14, author = {Jacques Carette and Gerardo Ortiz and Amr Sabry}, title = {Symbolic Execution of HadamardToffoli Quantum Circuits}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {1426}, doi = {10.1145/3571786.3573018}, year = {2023}, } Publisher's Version Published Artifact Artifacts Available 

Saraiva, João 
PEPM '23: "Efficient Embedding of Strategic ..."
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 rewriting and attribute grammars are two powerful programming techniques widely used in language engineering. The former relies on strategies to apply term rewrite rules in defining largescale language transformations, while the latter is suitable to express contextdependent language processing algorithms. These two techniques can be expressed and combined via a powerful navigation abstraction: generic zippers. This results in a concise zipperbased 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 recomputation. 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 stateoftheart Strafunski and Kiama libraries. Our first results show that we are competitive against those two well established libraries. @InProceedings{PEPM23p41, author = {José Nuno Macedo and Emanuel Rodrigues and Marcos Viera and João Saraiva}, title = {Efficient Embedding of Strategic Attribute Grammars via Memoization}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {4154}, doi = {10.1145/3571786.3573019}, year = {2023}, } Publisher's Version 

Tokuda, Ryo 
PEPM '23: "Generating Programs for Polynomial ..."
Generating Programs for Polynomial Multiplication with Correctness Assurance
Ryo Tokuda and Yukiyoshi Kameyama (University of Tsukuba, Japan) Programgeneration techniques prevail in domains that need high performance, such as linear algebra, image processing, and database. Yet, it is hard to generate highperformance programs with correctness assurance, and cryptography needs both. Masuda and Kameyama proposed a DSLbased framework for implementing a program generator, an analyzer, and a formula generator, and obtained an efficient and correct implementation of NumberTheoretic Transform (NTT) that is necessary for many cryptographic algorithms. This paper advances their study in two ways. First, we develop a generationandanalysis 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 postquantum cryptographic algorithms. @InProceedings{PEPM23p27, author = {Ryo Tokuda and Yukiyoshi Kameyama}, title = {Generating Programs for Polynomial Multiplication with Correctness Assurance}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {2740}, doi = {10.1145/3571786.3573017}, year = {2023}, } Publisher's Version 

Viera, Marcos 
PEPM '23: "Efficient Embedding of Strategic ..."
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 rewriting and attribute grammars are two powerful programming techniques widely used in language engineering. The former relies on strategies to apply term rewrite rules in defining largescale language transformations, while the latter is suitable to express contextdependent language processing algorithms. These two techniques can be expressed and combined via a powerful navigation abstraction: generic zippers. This results in a concise zipperbased 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 recomputation. 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 stateoftheart Strafunski and Kiama libraries. Our first results show that we are competitive against those two well established libraries. @InProceedings{PEPM23p41, author = {José Nuno Macedo and Emanuel Rodrigues and Marcos Viera and João Saraiva}, title = {Efficient Embedding of Strategic Attribute Grammars via Memoization}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {4154}, doi = {10.1145/3571786.3573019}, year = {2023}, } Publisher's Version 
14 authors
proc time: 3.13