Powered by
2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2019),
January 14–15, 2019,
Cascais, Portugal
2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2019)
Frontmatter
Message from the Chairs
We are pleased to present the proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2019), held in Cascais, Lisbon, January 14–15th, 2019, in affiliation with the annual Symposium on Principles of Programming Languages (POPL 2019). 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.
Papers
A Simpler Lambda Calculus
Barry Jay
(University of Technology Sydney, Australia)
Closure calculus is simpler than pure lambda-calculus as it does not mention free variables or index manipulation, variable renaming, implicit substitution, or any other meta-theory. Further, all programs, even recursive ones, can be expressed as normal forms. Third, there are reduction-preserving translations to calculi built from combinations of operators, in the style of combinatory logic. These improvements are achieved without sacrificing three fundamental properties of lambda-calculus, being a confluent rewriting system, supporting the Turing computable numerical functions, and supporting simple typing.
@InProceedings{PEPM19p1,
author = {Barry Jay},
title = {A Simpler Lambda Calculus},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {1--9},
doi = {10.1145/3294032.3294085},
year = {2019},
}
Publisher's Version
Method Name Suggestion with Hierarchical Attention Networks
Sihan Xu,
Sen Zhang,
Weijing Wang,
Xinya Cao,
Chenkai Guo, and
Jing Xu
(Nankai University, China)
Method Rename has been a widely used refactoring operation that improves program
comprehension and maintenance. Descriptive method names that summarize
functionalities of source code can facilitate program comprehension. Much
research has been done to suggest method names through source code
summarization. However, unlike natural language, a code snippet consists of
basic blocks organized by complicated structures. In this work, we observe a
hierarchical structure --- tokens form basic blocks and basic blocks form a code
snippet. Based on this observation, we exploit a hierarchical attention network
to learn the representation of methods. Specifically, we apply two-level
attention mechanism to learn the importance of each token in a basic block and
that of a basic block in a method respectively. We evaluated our approach on 10
open source repositories and compared it against three state-of-the-art
approaches. The results on these open-source data show the superiority of our
hierarchical attention networks in terms of effectiveness.
@InProceedings{PEPM19p10,
author = {Sihan Xu and Sen Zhang and Weijing Wang and Xinya Cao and Chenkai Guo and Jing Xu},
title = {Method Name Suggestion with Hierarchical Attention Networks},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {10--21},
doi = {10.1145/3294032.3294079},
year = {2019},
}
Publisher's Version
Reduction from Branching-Time Property Verification of Higher-Order Programs to HFL Validity Checking
Keiichi Watanabe,
Takeshi Tsukada,
Hiroki Oshikawa, and
Naoki Kobayashi
(University of Tokyo, Japan)
Various methods have recently been proposed for temporal property verification of higher-order programs. In those methods, however, either temporal properties were limited to linear-time ones, or target programs were limited to finite-data programs. In this paper, we extend Kobayashi et al.'s recent method for verification of linear-time temporal properties based on HFLZ model checking, to deal with branching-time properties. We formalize branching-time property verification problems as an extension of HORS model checking called HORSZ model checking, present a sound and complete reduction to validity checking of (modal-free) HFLZ formulas, and prove its correctness. The correctness of the reduction subsumes the decidability of HORS model checking. The HFLZ formula obtained by the reduction from a HORSZ model checking problem can be considered a kind of verification condition for the orignal model checking problem. We also discuss interactive and automated methods for discharging the verification condition.
@InProceedings{PEPM19p22,
author = {Keiichi Watanabe and Takeshi Tsukada and Hiroki Oshikawa and Naoki Kobayashi},
title = {Reduction from Branching-Time Property Verification of Higher-Order Programs to HFL Validity Checking},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {22--34},
doi = {10.1145/3294032.3294077},
year = {2019},
}
Publisher's Version
Typed Parsing and Unparsing for Untyped Regular Expression Engines
Gabriel Radanne
(University of Freiburg, Germany)
Regular expressions are used for a wide variety of purposes
from web-page input validation to log file crawling.
Very often, they are used not only to match strings, but
also to extract data from them.
Unfortunately, most regular expression engines
only return a list of the substrings captured by the regular
expression. The data has to be extracted from the
matched substrings to be validated and transformed manually into
a more structured format.
For richer classes of grammars like CFGs, such issues
can be solved using type-indexed combinators.
Most combinator libraries provide
a monadic API to track
the type returned by the parser through easy-to-use combinators.
This allows users to
transform the input into a custom data-structure and go through
complex validations as they describe their grammar.
In this paper, we present the Tyre library which provides
type-indexed combinators for regular languages.
Our combinators provide type-safe extraction
while delegating the task of substring matching to a preexisting
regular expression engine.
To do this, we use a two layer approach where the typed
layer sits on top of an untyped layer.
This technique is also amenable to several extensions, such as
routing, unparsing and static generation of the extraction code.
We also provide a syntax extension, which recovers
the familiar and compact syntax of regular expressions.
We implemented this technique in a very concise
manner and evaluated its usefulness on two practical examples.
@InProceedings{PEPM19p35,
author = {Gabriel Radanne},
title = {Typed Parsing and Unparsing for Untyped Regular Expression Engines},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {35--46},
doi = {10.1145/3294032.3294082},
year = {2019},
}
Publisher's Version
Info
Combining Higher-Order Model Checking with Refinement Type Inference
Ryosuke Sato,
Naoki Iwayama, and
Naoki Kobayashi
(Kyushu University, Japan; University of Tokyo, Japan)
There have been two major approaches to fully automated verification of higher-order functional programs:
higher-order model checking and refinement type inference.
The former approach is precise, but suffers from a bottleneck in the predicate discovery phase.
The latter approach is generally faster than the former,
thanks to the recent advances in constrained Horn clause (CHC) solving,
but is imprecise, in that it rejects some valid programs.
To take the best of the two approaches, we refine the higher-order model checking approach,
by employing CHC solving in the predicate discovery phase. We have
implemented the new approach
and confirmed that the new system can verify more programs than
those based on the previous two approaches.
@InProceedings{PEPM19p47,
author = {Ryosuke Sato and Naoki Iwayama and Naoki Kobayashi},
title = {Combining Higher-Order Model Checking with Refinement Type Inference},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {47--53},
doi = {10.1145/3294032.3294081},
year = {2019},
}
Publisher's Version
Control Flow Obfuscation via CPS Transformation
Kenny Zhuo Ming Lu
(Nanyang Polytechnic, Singapore)
Control flow obfuscation protects software from
being reverse-engineered by altering the control flow transfer without
without changing the software's run-time semantics.
We propose a new control flow obfuscation technique
by rewriting the source program in the continuation passing style (CPS).
The continuation is encoded through higher order
combinators and function pointers at the
target language level. As a result, the original control
flow graph is fragmented which makes any software tampering attempt through binary
static analysis hard. We implemented a prototype which performs
obfuscation on C source codes. The benchmark shows
that this approach is practical compared to existing techniques.
@InProceedings{PEPM19p54,
author = {Kenny Zhuo Ming Lu},
title = {Control Flow Obfuscation via CPS Transformation},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {54--60},
doi = {10.1145/3294032.3294083},
year = {2019},
}
Publisher's Version
Extracting a Call-by-Name Partial Evaluator from a Proof of Termination
Kenichi Asai
(Ochanomizu University, Japan)
It is well known that the computational content of a termination proof
of a calculus is an interpreter that computes the result of an input
term.
Traditionally, such extraction has been tried for a calculus with
deterministic reduction rules, producing the result as a value, i.e.,
in weak head normal form where no redexes are reduced under lambda.
In this paper, we consider non-deterministic reduction rules where any
redexes can be reduced, even the ones under lambda, and extract a
partial evaluator, rather than an interpreter, that produces the
result in normal form.
We formalize a call-by-name, simply-typed, lambda calculus in the
Agda proof assistant and prove its termination using a logical
predicate.
We observe that the extracted program can be regarded as an online
partial evaluator and present future perspectives about how we can
extend the framework to a call-by-value calculus.
@InProceedings{PEPM19p61,
author = {Kenichi Asai},
title = {Extracting a Call-by-Name Partial Evaluator from a Proof of Termination},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {61--67},
doi = {10.1145/3294032.3294084},
year = {2019},
}
Publisher's Version
Info
Futures and Promises in Haskell and Scala
Tamino Dauth and
Martin Sulzmann
(Karlsruhe University of Applied Sciences, Germany)
Futures and promises are a high-level concurrency construct to aid the user in writing scalable and correct asynchronous programs.
We introduce a simple core language based on which we can derive a rich set of future and promise features.
We discuss ways to implement the core features via shared-state concurrency
making either use of Software Transactional Memory,
an elementary lock-based primitive,
or an atomic compare-and-swap operation.
The approach has been fully implemented in Haskell and Scala.
For both languages, we provide empirical evidence of the effectiveness of our method.
We consider program transformations in the context of futures and promises
and observe potential problems in existing Scala-based libraries.
@InProceedings{PEPM19p68,
author = {Tamino Dauth and Martin Sulzmann},
title = {Futures and Promises in Haskell and Scala},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {68--74},
doi = {10.1145/3294032.3294080},
year = {2019},
}
Publisher's Version
Generating Mutually Recursive Definitions
Jeremy Yallop and
Oleg Kiselyov
(University of Cambridge, UK; Tohoku University, Japan)
Many functional programs — state machines [Krishnamurthi 2006], top-down and bottom-up parsers [Hinze and Paterson 2003; Hutton and Meijer 1996], evaluators [Abelson et al. 1984], GUI initialization graphs [Syme 2006], &c. — are conveniently expressed as groups of mutually recursive bindings. One therefore expects program generators, such as those written in MetaOCaml, to be able to build programs with mutual recursion.
Unfortunately, currently MetaOCaml can only build recursive groups whose size is hard-coded in the generating program. The general case requires something other than quotation, and seemingly weakens static guarantees on the resulting code. We describe the challenges and propose a new language construct for assuredly generating binding groups of arbitrary size – illustrating with a collection of examples for mutual, n-ary, heterogeneous, value and polymorphic recursion.
@InProceedings{PEPM19p75,
author = {Jeremy Yallop and Oleg Kiselyov},
title = {Generating Mutually Recursive Definitions},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {75--81},
doi = {10.1145/3294032.3294078},
year = {2019},
}
Publisher's Version
proc time: 0.92