Term rewriting for normalization by evaluation.

DOI10.1016/S0890-5401(03)00014-2MaRDI QIDQ1401941zbMATH OpenFDO

Authors Ulrich Berger, Matthias Eberl, Helmut Schwichtenberg

Publication date 19 August 2003

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

Full work available at URL https://doi.org/10.1016/S0890-5401(03)00014-2

zbMATH Keywords

\(\lambda\)-calculus

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1757129
• Approximation and normalization results for typeable term rewriting systems
• Operational aspects of untyped Normalisation by Evaluation
• scientific article; zbMATH DE number 2090724
• Foundations of Software Science and Computation Structures

Cites work

• Categorical reconstruction of a reduction free normalization proof
• Categories for Types
• scientific article; zbMATH DE number 3959364 (Why is no real title available?)
• scientific article; zbMATH DE number 1487847 (Why is no real title available?)
• scientific article; zbMATH DE number 1552509 (Why is no real title available?)
• scientific article; zbMATH DE number 1405571 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• Intuitionistic model constructions and normalization proofs
• LCF considered as a programming language
• Recursive functions of symbolic expressions and their computation by machine, Part I

Cited in

(12)

• Realizability interpretation of proofs in constructive analysis
• Some general results about proof normalization
• Light Dialectica program extraction from a classical Fibonacci proof
• A compiled implementation of normalisation by evaluation
• There is no best \(\beta \)-normalization strategy for higher-order reasoners
• A Compiled Implementation of Normalization by Evaluation
• New developments in environment machines
• Experimenting with deduction modulo
• Normalization by Evaluation for Martin-Löf Type Theory with One Universe
• Program extraction in exact real arithmetic
• Normalization by leftmost innermost rewriting
• Program extraction from normalization proofs

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1401941)