Skip to main content
1 of 2

Normalization-by-evaluation algorithm which results in beta-eta normal form

Usual NbE algorithms, which use (P)HOAS to embed terms to a host language constructs, results in a beta-normal form of a terms.

Is there algorithms to (efficiently) exploit host language constructs to normalize terms to beta-eta normal form?