Powered by
ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2018),
January 8–9, 2018,
Los Angeles, CA, USA
ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2018)
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.
@InProceedings{PEPM18p1,
author = {Jan Midtgaard},
title = {Developments in Property-Based Testing (Invited Talk)},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {1--1},
doi = {10.1145/3168896},
year = {2018},
}
Publisher's Version
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.
@InProceedings{PEPM18p2,
author = {Akifumi Imanishi and Kohei Suenaga and Atsushi Igarashi},
title = {A Guess-and-Assume Approach to Loop Fusion for Program Verification},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {2--14},
doi = {10.1145/3162070},
year = {2018},
}
Publisher's Version
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.
@InProceedings{PEPM18p15,
author = {David Broman and Jeremy G. Siek},
title = {Gradually Typed Symbolic Expressions},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {15--29},
doi = {10.1145/3162068},
year = {2018},
}
Publisher's Version
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.
@InProceedings{PEPM18p30,
author = {Ben Greenman and Zeina Migeed},
title = {On the Cost of Type-Tag Soundness},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {30--39},
doi = {10.1145/3162066},
year = {2018},
}
Publisher's Version
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.
@InProceedings{PEPM18p40,
author = {Kenichi Asai and Chihiro Uehara},
title = {Selective CPS Transformation for Shift and Reset},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {40--52},
doi = {10.1145/3162069},
year = {2018},
}
Publisher's Version
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.
@InProceedings{PEPM18p53,
author = {Duncan Mitchell and L. Thomas van Binsbergen and Blake Loring and Johannes Kinder},
title = {Checking Cryptographic API Usage with Composable Annotations (Short Paper)},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {53--59},
doi = {10.1145/3162071},
year = {2018},
}
Publisher's Version
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.
@InProceedings{PEPM18p60,
author = {Takahisa Watanabe and Yukiyoshi Kameyama},
title = {Program Generation for ML Modules (Short Paper)},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {60--66},
doi = {10.1145/3162072},
year = {2018},
}
Publisher's Version
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.
@InProceedings{PEPM18p67,
author = {Barry Jay},
title = {Recursive Programs in Normal Form (Short Paper)},
booktitle = {Proc.\ PEPM},
publisher = {ACM},
pages = {67--73},
doi = {10.1145/3162067},
year = {2018},
}
Publisher's Version
proc time: 1.41