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 - 10:55|
Gabriel SchererNortheastern University
|10:55 - 11:20|
Danko IlikTrusted Labs
|11:20 - 11:45|
|11:45 - 12:10|