From Self-Interpreters to Normalization by Evaluation

Mathieu Boespflug (1, 2)

1 LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
2 TYPICAL - Types, Logic and computing

We characterize normalization by evaluation as the composition of a self-interpreter with a self-reducer using a special representation scheme, in the sense of Mogensen (1992). We do so by deriving in a systematic way an untyped normalization by evaluation algorithm from a standard interpreter for the λ-calculus. The derived algorithm is not novel and indeed other published algorithms may be obtained in the same manner through appropriate adaptations to the representation scheme.

Domaines: Langage de programmation [cs.PL]; Logique en informatique [cs.LO]

Mathieu Boespflug. From Self-Interpreters to Normalization by Evaluation. 2009 Workshop on Normalization by Evaluation, Olivier Danvy, Aug 2009, Los Angeles, United States. ⟨inria-00434284⟩