
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
