POPL 2018 Co-Located Events
POPL 2018 Co-Located Events
Powered by
Conference Publishing Consulting

ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2018), January 8–9, 2018, Los Angeles, CA, USA

PEPM 2018 – Proceedings

Contents - Abstracts - Authors

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

Title Page

Message from the Chairs
We are pleased to present the proceedings of the 2018 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2018), held in Los Angeles, California, January 8–9th, 2018, in affiliation with the annual Symposium on Principles of Programming Languages (POPL 2018). 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.
Developments in Property-Based Testing (Invited Talk)
Jan Midtgaard
(University of Southern Denmark, Denmark)
Property-based testing (aka. QuickCheck) is a successful au- tomated testing approach originating in the programming language community (Claessen-Hughes:ICFP00). It unites the well-known idea of randomized testing with that of en- suring program-specific properties akin to those encoun- tered within verification and theorem proving. Starting as a Haskell library the approach has grown to become language independent with ports to over 30 different programming languages. Over the years property-based testing has been used to pinpoint an impressive amount of software errors in a multitude of settings, initially within academia but more and more so also in the software industry. In this talk I will first recall the basic concepts of property- based testing and then cover a couple of recent applications, while sharing some of the folklore and community know- how. This includes quite a bit of symbolic program manipu- lation at the heart of the PEPM community. I will then offer a personal perspective on the approach, both in terms of programming language theory and software engineering.
Publisher's Version Article Search
A Guess-and-Assume Approach to Loop Fusion for Program Verification
Akifumi Imanishi, Kohei Suenaga, and Atsushi Igarashi
(Kyoto University, Japan)

Loop fusion—a program transformation to merge multiple consecutive loops into a single one—has been studied mainly for compiler optimization. In this paper, we propose a new loop fusion strategy, which can fuse any loops—even loops with data dependence—and show that it is useful for program verification because it can simplify loop invariants.

The crux of our loop fusion is the following observation: if the state after the first loop were known, the two loop bodies could be computed at the same time without suffering from data dependence by renaming program variables. Our loop fusion produces a program that guesses the unknown state after the first loop nondeterministically, executes the fused loop where variables are renamed, compares the guessed state and the state actually computed by the fused loop, and, if they do not match, diverges. The last two steps of comparison and divergence are crucial to preserve partial correctness. We call our approach “guess-and-assume” because, in addition to the first step to guess, the last two steps can be expressed by the pseudo-instruction assume, used in program verification.

We formalize our loop fusion for a simple imperative language and prove that it preserves partial correctness. We further extend the “guess-and-assume” technique to reversing loop execution, which is useful to verify a certain type of consecutive loops. Finally, we confirm by experiments that our transformation techniques are indeed effective for state-of-the-art model checkers to verify a few small programs that they could not.

Publisher's Version Article Search
Gradually Typed Symbolic Expressions
David Broman and Jeremy G. Siek
(KTH, Sweden; Indiana University, USA)

Embedding a domain-specific language (DSL) in a general purpose host language is an efficient way to develop a new DSL. Various kinds of languages and paradigms can be used as host languages, including object-oriented, functional, statically typed, and dynamically typed variants, all having their pros and cons. For deep embedding, statically typed languages enable early checking and potentially good DSL error messages, instead of reporting runtime errors. Dynamically typed languages, on the other hand, enable flexible transformations, thus avoiding extensive boilerplate code. In this paper, we introduce the concept of gradually typed symbolic expressions that mix static and dynamic typing for symbolic data. The key idea is to combine the strengths of dynamic and static typing in the context of deep embedding of DSLs. We define a gradually typed calculus λ<>, formalize its type system and dynamic semantics, and prove type safety. We introduce a host language called Modelyze that is based on λ<>, and evaluate the approach by embedding a series of equation-based domain-specific modeling languages, all within the domain of physical modeling and simulation.

Publisher's Version Article Search
On the Cost of Type-Tag Soundness
Ben Greenman and Zeina Migeed
(Northeastern University, USA)
Gradual typing systems ensure type soundness by transforming static type annotations into run-time checks. These checks provide semantic guarantees, but may come at a large cost in performance. In particular, recent work by Takikawa et al. suggests that enforcing a conventional form of type soundness may slow a program by two orders of magnitude. Since different gradual typing systems satisfy different notions of soundness, the question then arises: what is the cost of such varying notions of soundness? This paper answers an instance of this question by applying Takikawa et al.'s evaluation method to Reticulated Python, which satisfies a notion of type-tag soundness. We find that the cost of soundness in Reticulated is at most one order of magnitude, and increases linearly with the number of type annotations.
Publisher's Version Article Search Info
Selective CPS Transformation for Shift and Reset
Kenichi Asai and Chihiro Uehara
(Ochanomizu University, Japan)
This paper presents a selective CPS transformation for a program that uses control operators, shift and reset, introduced by Danvy and Filinski. By selectively CPS-transforming a program, we can execute a program with shift and reset in a standard functional language without support for control operators. We introduce a constraint-based type inference system that annotates the parts that are captured by shift and thus require CPS transformation. We show that the best annotation does not exist in general, and present a constraint solving algorithm that is reasonably efficient. The selective CPS transformation is defined over annotated terms and its correctness is proven. Finally, experimental results show that selective CPS transformation does improve performance compared to the standard CPS transformation.
Publisher's Version Article Search
Checking Cryptographic API Usage with Composable Annotations (Short Paper)
Duncan Mitchell, L. Thomas van Binsbergen, Blake Loring, and Johannes Kinder
(Royal Holloway University of London, UK)

Developers of applications relying on cryptographic libraries can easily make mistakes in their use. Popular dynamic languages such as JavaScript make testing or verifying such applications particularly challenging. In this paper, we present our ongoing work toward a methodology for automatically checking security properties in JavaScript code. Our main idea is to attach security annotations to values that encode properties of interest. We illustrate our idea using examples and, as an initial step in our line of work, we present a formalization of security annotations in a statically typed lambda calculus. As next steps, we will translate our annotations to a dynamically typed formalization of JavaScript such as λJS and implement a runtime checked type extension using code instrumentation for full JavaScript.

Publisher's Version Article Search
Program Generation for ML Modules (Short Paper)
Takahisa Watanabe and Yukiyoshi Kameyama
(University of Tsukuba, Japan)
Program generation has been successful in various domains which need high performance and high productivity. Yet, programming-language supports for program generation need further improvement. An important omission is the functionality of generating modules in a type safe way. Inoue et al. have addressed this issue in 2016, but investigated only a few examples. We propose a language as an extension of (a small subset of) MetaOCaml in which one can manipulate and generate code of a module, and implement it based on a simple translation to MetaOCaml. We show that our language solves the performance problem in functor applications pointed out by Inoue et al., and that it provides a suitable basis for writing code generators for modules.
Publisher's Version Article Search
Recursive Programs in Normal Form (Short Paper)
Barry Jay
(University of Technology Sydney, Australia)
Recursive programs can now be expressed as normal forms within some rewriting systems, including traditional combinatory logic, a new variant of lambda-calculus called closure calculus, and recent variants of combinatory logic that support queries of internal program structure. In all these settings, partial evaluation of primitive recursive functions, such as addition, can reduce open terms to normal form without fear of non-termination. In those calculi where queries of program structure are supported, program optimisations that are expressed as non-standard rewriting rules can be represented as functions in the calculus, without any need for quotation or other meta-theory.
Publisher's Version Article Search

proc time: 3.72