POPL 2017
Sun 15 - Sat 21 January 2017
Thu 19 Jan 2017 11:45 - 12:10 at Auditorium - Type Systems 2 Chair(s): Andrew D. Gordon

Many popular languages have a self-interpreter, that is, an interpreter for the language written in itself. So far, work on polymorphically-typed self-interpreters has concentrated on self-recognizers that merely recover a program from its representation. A larger and until now unsolved challenge is to implement a polymorphically-typed self-evaluator that evaluates the represented program and produces a representation of the result. We present ourlang, the first λ-calculus that supports a polymorphically-typed self-evaluator. Our calculus extends Fω with recursive types and intensional type functions and has decidable type checking. Our key innovation is a novel implementation of type equality proofs that enables us to define a versatile representation of programs. Our results establish a new category of languages that can support polymorphically-typed self-evaluators.

Thu 19 Jan (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:10: POPL - Type Systems 2 at Auditorium
Chair(s): Andrew D. GordonMicrosoft Research and University of Edinburgh
POPL-2017-papers10:30 - 10:55
Gabriel SchererNortheastern University
POPL-2017-papers10:55 - 11:20
Danko IlikTrusted Labs
POPL-2017-papers11:20 - 11:45
POPL-2017-papers11:45 - 12:10
Matt BrownUCLA, Jens PalsbergUniversity of California, Los Angeles