Term rewriting for normalization by evaluation.

DOI10.1016/S0890-5401(03)00014-2zbMath1054.68078MaRDI QIDQ1401941

Helmut Schwichtenberg, Ulrich Berger, Matthias Eberl

Publication date: 19 August 2003

Published in: Information and Computation (Search for Journal in Brave)

zbMATH Keywords

\(\lambda\)-calculus

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Grammars and rewriting systems (68Q42)

Related Items (10)

A compiled implementation of normalisation by evaluation ⋮ Some general results about proof normalization ⋮ A Compiled Implementation of Normalization by Evaluation ⋮ New Developments in Environment Machines ⋮ Program extraction in exact real arithmetic ⋮ Experimenting with Deduction Modulo ⋮ Realizability interpretation of proofs in constructive analysis ⋮ Light Dialectica Program Extraction from a Classical Fibonacci Proof ⋮ Normalization by Evaluation for Martin-Löf Type Theory with One Universe ⋮ Program extraction from normalization proofs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• LCF considered as a programming language
• Intuitionistic model constructions and normalization proofs
• Recursive functions of symbolic expressions and their computation by machine, Part I
• Categories for Types
• Categorical reconstruction of a reduction free normalization proof

This page was built for publication: Term rewriting for normalization by evaluation.