Term rewriting for normalization by evaluation.
From MaRDI portal
Publication:1401941
Recommendations
Cites work
- 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?)
- Categorical reconstruction of a reduction free normalization proof
- Categories for Types
- 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)- Normalization by leftmost innermost rewriting
- Realizability interpretation of proofs in constructive analysis
- Program extraction in exact real arithmetic
- New developments in environment machines
- Some general results about proof normalization
- Normalization by Evaluation for Martin-Löf Type Theory with One Universe
- 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)
