Term rewriting for normalization by evaluation.
From MaRDI portal
Publication:1401941
DOI10.1016/S0890-5401(03)00014-2zbMATH Open1054.68078MaRDI QIDQ1401941FDOQ1401941
Authors: Ulrich Berger, Matthias Eberl, Helmut Schwichtenberg 
Publication date: 19 August 2003
Published in: Information and Computation (Search for Journal in Brave)
Recommendations
Cites Work
- LCF considered as a programming language
- Title not available (Why is that?)
- Categories for Types
- Categorical reconstruction of a reduction free normalization proof
- Recursive functions of symbolic expressions and their computation by machine, Part I
- Title not available (Why is that?)
- Title not available (Why is that?)
- Intuitionistic model constructions and normalization proofs
- Title not available (Why is that?)
- Title not available (Why is that?)
Cited In (12)
- Normalization by leftmost innermost rewriting
- Realizability interpretation of proofs in constructive analysis
- Program extraction in exact real arithmetic
- New developments in environment machines
- Normalization by Evaluation for Martin-Löf Type Theory with One Universe
- Some general results about proof normalization
- A compiled implementation of normalisation by evaluation
- Experimenting with deduction modulo
- A Compiled Implementation of Normalization by Evaluation
- There is no best \(\beta \)-normalization strategy for higher-order reasoners
- Light Dialectica program extraction from a classical Fibonacci proof
- 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)
