PEPM 2019- Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation

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.

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.

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.

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.

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.

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.

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.

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.

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.