Paper Info
Title
Normalisation by Evaluation
Abstract
. We extend normalization by evaluation (first presented in[4]) from the pure typed -calculus to general higher type term rewritesystems. This work also gives a theoretical explanation of the normalizationalgorithm implemented in the Minlog system.1 IntroductionIn interactive proof systems it is crucial to have a term rewriting machineryavailable, in order to ease the burden of equational reasoning. Quite often termrewriting can be reduced to normalization and therefore it is essential...
Year
DOI
Venue
1998
10.1007/3-540-49254-2_4
New Hardware Design Methods
Keywords
Field
DocType
theoretical explanation,general higher type term,minlog system,normalization algorithm
Normalization (statistics),Normalisation by evaluation,Interactive proof system,Partial evaluation,Algorithm,Calculus,Mathematics
Conference
ISBN
Citations 
PageRank 
3-540-65461-5
28
1.75
References 
Authors
7
3
Name
Order
Citations
PageRank
Ulrich Berger119718.25
Matthias Eberl2423.37
Helmut Schwichtenberg337344.83