Skip to Main content Skip to Navigation
New interface
Conference papers

From Self-Interpreters to Normalization by Evaluation

Mathieu Boespflug 1, 2 
2 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
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 Connect in order to contact the contributor
Submitted on : Saturday, November 21, 2009 - 10:12:35 PM
Last modification on : Friday, February 4, 2022 - 3:16:54 AM
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