Skip to Main content Skip to Navigation
Conference papers

From Self-Interpreters to Normalization by Evaluation

Mathieu Boespflug 1, 2
2 TYPICAL - Types, Logic and computing
Inria Saclay - Ile de France, LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
Abstract : 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.
Complete list of metadata

Cited literature [4 references]  Display  Hide  Download
Contributor : Mathieu Boespflug <>
Submitted on : Saturday, November 21, 2009 - 10:12:35 PM
Last modification on : Thursday, March 5, 2020 - 6:22:04 PM
Long-term archiving on: : Thursday, June 17, 2010 - 9:18:58 PM


Publisher files allowed on an open archive


  • HAL Id : inria-00434284, version 1
  • ARXIV : 0911.4203



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⟩



Record views


Files downloads