Workshop PEPM 2018 – Author Index 
Contents 
Abstracts 
Authors

Asai, Kenichi 
PEPM '18: "Selective CPS Transformation ..."
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 CPStransforming a program, we can execute a program with shift and reset in a standard functional language without support for control operators. We introduce a constraintbased 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 = {4052}, doi = {10.1145/3162069}, year = {2018}, } Publisher's Version Article Search 

Broman, David 
PEPM '18: "Gradually Typed Symbolic Expressions ..."
Gradually Typed Symbolic Expressions
David Broman and Jeremy G. Siek (KTH, Sweden; Indiana University, USA) Embedding a domainspecific 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 objectoriented, 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 equationbased domainspecific 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 = {1529}, doi = {10.1145/3162068}, year = {2018}, } Publisher's Version Article Search 

Greenman, Ben 
PEPM '18: "On the Cost of TypeTag Soundness ..."
On the Cost of TypeTag Soundness
Ben Greenman and Zeina Migeed (Northeastern University, USA) Gradual typing systems ensure type soundness by transforming static type annotations into runtime 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 typetag 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 TypeTag Soundness}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {3039}, doi = {10.1145/3162066}, year = {2018}, } Publisher's Version Article Search Info 

Igarashi, Atsushi 
PEPM '18: "A GuessandAssume Approach ..."
A GuessandAssume 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 “guessandassume” because, in addition to the first step to guess, the last two steps can be expressed by the pseudoinstruction 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 “guessandassume” 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 stateoftheart 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 GuessandAssume Approach to Loop Fusion for Program Verification}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {214}, doi = {10.1145/3162070}, year = {2018}, } Publisher's Version Article Search 

Imanishi, Akifumi 
PEPM '18: "A GuessandAssume Approach ..."
A GuessandAssume 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 “guessandassume” because, in addition to the first step to guess, the last two steps can be expressed by the pseudoinstruction 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 “guessandassume” 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 stateoftheart 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 GuessandAssume Approach to Loop Fusion for Program Verification}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {214}, doi = {10.1145/3162070}, year = {2018}, } Publisher's Version Article Search 

Jay, Barry 
PEPM '18: "Recursive Programs in Normal ..."
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 lambdacalculus 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 nontermination. In those calculi where queries of program structure are supported, program optimisations that are expressed as nonstandard rewriting rules can be represented as functions in the calculus, without any need for quotation or other metatheory. @InProceedings{PEPM18p67, author = {Barry Jay}, title = {Recursive Programs in Normal Form (Short Paper)}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {6773}, doi = {10.1145/3162067}, year = {2018}, } Publisher's Version Article Search 

Kameyama, Yukiyoshi 
PEPM '18: "Program Generation for ML ..."
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, programminglanguage 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 = {6066}, doi = {10.1145/3162072}, year = {2018}, } Publisher's Version Article Search 

Kinder, Johannes 
PEPM '18: "Checking Cryptographic API ..."
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 = {5359}, doi = {10.1145/3162071}, year = {2018}, } Publisher's Version Article Search 

Loring, Blake 
PEPM '18: "Checking Cryptographic API ..."
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 = {5359}, doi = {10.1145/3162071}, year = {2018}, } Publisher's Version Article Search 

Midtgaard, Jan 
PEPM '18: "Developments in PropertyBased ..."
Developments in PropertyBased Testing (Invited Talk)
Jan Midtgaard (University of Southern Denmark, Denmark) Propertybased testing (aka. QuickCheck) is a successful au tomated testing approach originating in the programming language community (ClaessenHughes:ICFP00). It unites the wellknown idea of randomized testing with that of en suring programspecific 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 propertybased 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 PropertyBased Testing (Invited Talk)}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {11}, doi = {10.1145/3168896}, year = {2018}, } Publisher's Version Article Search 

Migeed, Zeina 
PEPM '18: "On the Cost of TypeTag Soundness ..."
On the Cost of TypeTag Soundness
Ben Greenman and Zeina Migeed (Northeastern University, USA) Gradual typing systems ensure type soundness by transforming static type annotations into runtime 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 typetag 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 TypeTag Soundness}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {3039}, doi = {10.1145/3162066}, year = {2018}, } Publisher's Version Article Search Info 

Mitchell, Duncan 
PEPM '18: "Checking Cryptographic API ..."
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 = {5359}, doi = {10.1145/3162071}, year = {2018}, } Publisher's Version Article Search 

Siek, Jeremy G. 
PEPM '18: "Gradually Typed Symbolic Expressions ..."
Gradually Typed Symbolic Expressions
David Broman and Jeremy G. Siek (KTH, Sweden; Indiana University, USA) Embedding a domainspecific 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 objectoriented, 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 equationbased domainspecific 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 = {1529}, doi = {10.1145/3162068}, year = {2018}, } Publisher's Version Article Search 

Suenaga, Kohei 
PEPM '18: "A GuessandAssume Approach ..."
A GuessandAssume 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 “guessandassume” because, in addition to the first step to guess, the last two steps can be expressed by the pseudoinstruction 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 “guessandassume” 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 stateoftheart 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 GuessandAssume Approach to Loop Fusion for Program Verification}, booktitle = {Proc.\ PEPM}, publisher = {ACM}, pages = {214}, doi = {10.1145/3162070}, year = {2018}, } Publisher's Version Article Search 

Uehara, Chihiro 
PEPM '18: "Selective CPS Transformation ..."
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 CPStransforming a program, we can execute a program with shift and reset in a standard functional language without support for control operators. We introduce a constraintbased 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 = {4052}, doi = {10.1145/3162069}, year = {2018}, } Publisher's Version Article Search 

Van Binsbergen, L. Thomas 
PEPM '18: "Checking Cryptographic API ..."
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 = {5359}, doi = {10.1145/3162071}, year = {2018}, } Publisher's Version Article Search 

Watanabe, Takahisa 
PEPM '18: "Program Generation for ML ..."
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, programminglanguage 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 = {6066}, doi = {10.1145/3162072}, year = {2018}, } Publisher's Version Article Search 
17 authors
proc time: 0.42