Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Mon 14 Jan 2019 16:00 - 17:00 at Sala X - Session 3 Chair(s): Atsushi Igarashi

The 1993 book of Jones, Gomard, and Sestoft talked about typed partial evaluators and called for a type system that supports them. Such a type system should be polymorphic, enable typed representation of programs, and allow self-application. However, the book left the details as an exercise. A couple of decades later, we can finally declare this exercise fully solved. I will describe the long and winding road to settling how much polymorphism is needed, how to represent programs, and how to support Jones optimality. My solution to the exercise is joint work with Matt Brown and uses an extension of F-omega that goes beyond the type systems of most languages. Still, if we use a mainstream typed language such as Java, we can get some of the benefits, as I will discuss.

What is the Type of a Partial Evaluator? (doc.pdf)2.71MiB

Mon 14 Jan

Displayed time zone: Belfast change

16:00 - 17:30
Session 3PEPM at Sala X
Chair(s): Atsushi Igarashi Kyoto University, Japan
What Is the Type of a Partial Evaluator? (Invited Talk)
Jens Palsberg University of California, Los Angeles (UCLA)
File Attached
Combining Higher-Order Model Checking with Refinement Type Inference
Ryosuke Sato Kyushu University, Japan, Naoki Iwayama University of Tokyo, Japan, Naoki Kobayashi University of Tokyo, Japan