Name
Abstract | ||
|---|---|---|
We present a novel compiled approach to Normalisation by Evaluation (NBE) for ML-like languages. It supports efficient normalisation of open λ-terms with respect to β-reduction and rewrite rules. We have implemented NBE and show both a detailed formal model of our implementation and its verification in Isabelle. Finally we discuss how NBE is turned into a proof rule in Isabelle. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1017/S0956796812000019 | Theorem Proving in Higher Order Logics |
Keywords | Field | DocType |
detailed formal model,proof rule,ml-like language,efficient normalisation | Programming language,Normalisation by evaluation,Computer science | Journal |
Volume | Issue | ISSN |
22 | 1 | 0956-7968 |
Citations | PageRank | References |
10 | 0.78 | 13 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Klaus Aehlig | 1 | 123 | 12.08 |
| Florian Haftmann | 2 | 247 | 13.39 |
| Tobias Nipkow | 3 | 3056 | 232.28 |