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
Times are displayed in time zone: Greenwich Mean Time : Belfast change

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