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 | Type Systems 2POPL at Auditorium Chair(s): Andrew D. Gordon Microsoft Research and University of Edinburgh | ||
10:30 25mTalk | Deciding equivalence with sums and the empty type POPL Gabriel Scherer Northeastern University | ||
10:55 25mTalk | The exp-log normal form of types: Decomposing extensional equality and representing terms compactly POPL Danko Ilik Trusted Labs | ||
11:20 25mTalk | Contextual isomorphisms POPL | ||
11:45 25mTalk | Typed Self-Evaluation via Intensional Type Functions POPL | ||