Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

9

TPHOL
2008
IEEE

favoriteEmaildiscussreport

98views Automated Reasoning» more TPHOL 2008»

A Compiled Implementation of Normalization by Evaluation

13 years 11 months ago

A Compiled Implementation of Normalization by Evaluation

Download www.linta.de

We present a novel compiled approach to Normalization by Evaluation (NBE) for ML-like languages. It supports eﬃcient normalization of open λ-terms w.r.t. β-reduction and rewrite rules. We have implemented NBE and show both a detailed formal model of our implementation and its veriﬁcation in Isabelle. Finally we discuss how NBE is turned into a proof rule in Isabelle.

Klaus Aehlig, Florian Haftmann, Tobias Nipkow

Real-time Traffic

Artificial Intelligence | Eﬃcient Normalization | ML-like Languages | Rewrite Rules | TPHOL 2008 |

claim paper

Related Content

» Compilation of Head and Strong Reduction

» Conversion by Evaluation

» Implementation and Evaluation of OpenMP for Hitachi SR8000

» Performance Monitoring and Evaluation of a UPC Implementation on a NUMA Architecture

» The design implementation and evaluation of a compiler algorithm for CPU energy reduction

» Design Implementation and Evaluation of Optimizations in a JustinTime Compiler

» Shrinking Reductions in SMLNET

» An algebraic approach to the design of compilers for objectoriented languages

» High Speed MaxLogMAP Turbo SISO Decoder Implementation Using Branch Metric Normalization

Post Info
More Details (n/a)

Added	01 Jun 2010
Updated	01 Jun 2010
Type	Conference
Year	2008
Where	TPHOL
Authors	Klaus Aehlig, Florian Haftmann, Tobias Nipkow

Comments (0)