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

https://hal.inria.fr/inria-00434284
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

Files

selfnbe.pdf
Publisher files allowed on an open archive

Identifiers

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

Collections

Citation

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⟩

Share

Metrics

Record views

255

Files downloads

210