POPL 2021 Co-Located Events
POPL 2021 Co-Located Events

Title Page

Message from the Chairs
We are pleased to present the proceedings of the 2021 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2021), held January 18–19th, 2021, in aliation with the annual Symposium on Principles of Programming Languages (POPL 2021). (Originally POPL 2021 was originally to be held in Copenhagen, Denmark, but due to the COVID-19 pandemic, it was moved entirely online.) PEPM has a history dating 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, analysed, and transformed whilst establishing or maintaining important semantic properties. Relevant topics range 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.

A Type-Safe Structure Editor Calculus
Christian Godiksen, Thomas Herrmann, Hans Hüttel, Mikkel Korup Lauridsen, and Iman Owliaie
(Aalborg University, Denmark)
Structure editors make syntax errors impossible, but they still allow construction of programs with incomplete semantics, leading to program states that cannot be evaluated. We introduce a structure editor calculus for a simple functional programming language that allows for incomplete programs. Our editor expressions may interleave construction and evaluation of programs and can thus describe the history of the development of a program. We extend our editor calculus with types and define a resource-aware type system that prohibits editor expressions introducing type errors in the abstract syntax tree and prove that the type system is sound.

@InProceedings{PEPM21p1, author = {Christian Godiksen and Thomas Herrmann and Hans Hüttel and Mikkel Korup Lauridsen and Iman Owliaie}, title = {A Type-Safe Structure Editor Calculus}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {1--13}, doi = {10.1145/3441296.3441393}, year = {2021}, } Publisher's Version

Coq to C Translation with Partial Evaluation
Akira Tanaka
(AIST, Japan)
Coq proof assistant can be used to prove various properties of programs written in the Gallina language. It is also possible to translate Gallina programs to OCaml programs. However, OCaml is not suitable for low-level programs. Therefore, we are developing a Coq plugin for Gallina to C translation. This plugin transforms functions written in Gallina into a form as close to C as possible within Gallina. This transformation includes partial evaluation, which improves execution efficiency and eliminates polymorphism and dependent types. We can easily verify in Coq that this transformation does not change the execution result, and thus it is highly reliable. And Gallina functions after this transformation can be easily translated to C.

@InProceedings{PEPM21p14, author = {Akira Tanaka}, title = {Coq to C Translation with Partial Evaluation}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {14--31}, doi = {10.1145/3441296.3441394}, year = {2021}, } Publisher's Version

A Text-Based Syntax Completion Method using LR Parsing
Isao Sasano and Kwanghoon Choi
(Shibaura Institute of Technology, Japan; Chonnam National University, South Korea)
This paper presents a text-based syntax completion method using an LR parser. We propose formal definitions of candidate text to be completed based on the sentential forms, and we design algorithms for computing candidates through reductions in the LR parsing. This is in contrast to the existing methods that have not clearly stated what candidates they intend to produce. This is also different from a transformation approach using an LR parser, which transforms the grammar of the programming language, a burdensome task at this moment. The advantage of our method is that LR parsers can be adopted without modification, and a syntax completion system can be built using them, without incurring efforts. We implemented the algorithms as an Emacs server to demonstrate the feasibility of their application.

@InProceedings{PEPM21p32, author = {Isao Sasano and Kwanghoon Choi}, title = {A Text-Based Syntax Completion Method using LR Parsing}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {32--43}, doi = {10.1145/3441296.3441395}, year = {2021}, } Publisher's Version

Counterexample Generation for Program Verification Based on Ownership Refinement Types
Hideto Ueno, John Toman, Naoki Kobayashi, and Takeshi Tsukada
(University of Tokyo, Japan; Certora, USA; Chiba University, Japan)
Type-based program verification, which reduces program verification to type inference, has been used as a lightweight approach to automated program verification. Whilst it is often effective and faster than other methods such as model checking, the type-based approach often fails to provide useful information upon a failure of the verification. We address this problem for a recent type-based verification tool called ConSORT for imperative programs. Producing a useful error message is particularly challenging for ConSORT, as the underlying type system combines the notions of ownership, refinement types, and context-sensitivity. This paper proposes a method to produce error messages for ConSORT and reports an implementation and experimental results. The proposed method is potentially useful also for other type-based tools for automated program verification.

@InProceedings{PEPM21p44, author = {Hideto Ueno and John Toman and Naoki Kobayashi and Takeshi Tsukada}, title = {Counterexample Generation for Program Verification Based on Ownership Refinement Types}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {44--57}, doi = {10.1145/3441296.3441396}, year = {2021}, } Publisher's Version

Efficient Fair Conjunction for Structurally-Recursive Relations
Peter Lozov and Dmitry Boulytchev
(St. Petersburg State University, Russia; JetBrains Research, Russia)
We present a new, fair, conjunction evaluation strategy for relational programming language miniKanren. Unlike the original left-biased conjunction, our approach controls the order of conjunct execution based on the intrinsic properties of relation definitions. We present both the formal study of conjunction fairness and practical evaluation, which demonstrates the essential improvement in terms of both performance and convergence.

@InProceedings{PEPM21p58, author = {Peter Lozov and Dmitry Boulytchev}, title = {Efficient Fair Conjunction for Structurally-Recursive Relations}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {58--73}, doi = {10.1145/3441296.3441397}, year = {2021}, } Publisher's Version

Strictly Capturing Non-strict Closures
Zachary J. Sullivan, Paul Downen, and Zena M. Ariola
(University of Oregon, USA)
All functional languages need closures. Closure-conversion is a compiler transformation that embeds static code into the program for creating and manipulating closures, avoiding the need for special run-time closure support. For call-by-value languages, closure-conversion has been the focus of extensive studies concerning correctness, such as type preservation and contextual equivalence, and performance, such as space usage. Unfortunately, non-strict languages have been neglected in these studies. This paper aims to fill this gap.
We begin with both a call-by-name and a call-by-need source language whose semantics automatically generates closures at run-time. Next, we give type-preserving closure-conversions for these two non-strict languages into a lower-level target language without automatic closure generation at run-time. Despite the fact that our source languages are non-strict, we show that closures must be created eagerly, which requires a strict notion of product in the target language. We extend logical relation techniques used to prove compiler correctness for call-by-value languages, to apply to non-strict languages too. In doing so, we identify some important properties for reasoning about memoization with a heap.

@InProceedings{PEPM21p74, author = {Zachary J. Sullivan and Paul Downen and Zena M. Ariola}, title = {Strictly Capturing Non-strict Closures}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {74--89}, doi = {10.1145/3441296.3441398}, year = {2021}, } Publisher's Version