What Is the Type of a Partial Evaluator? (Invited Talk)
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 JanDisplayed time zone: Belfast change
16:00 - 17:30 | |||
16:00 60mTalk | What Is the Type of a Partial Evaluator? (Invited Talk) PEPM Jens Palsberg University of California, Los Angeles (UCLA) File Attached | ||
17:00 30mTalk | Combining Higher-Order Model Checking with Refinement Type Inference PEPM Ryosuke Sato Kyushu University, Japan, Naoki Iwayama University of Tokyo, Japan, Naoki Kobayashi University of Tokyo, Japan DOI | ||
