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 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:10
|Deciding equivalence with sums and the empty type|
Gabriel Scherer Northeastern University
|The exp-log normal form of types: Decomposing extensional equality and representing terms compactly|
Danko Ilik Trusted Labs
|Typed Self-Evaluation via Intensional Type Functions|