Name
Abstract | ||
|---|---|---|
We formalize two proofs of weak head normalization for the simply typed lambda-calculus in first-order minimal logic: one for normal-order reduction, and one for applicative-order reduction in the object language. Subsequently we use Kreisel's modified realizability to extract evaluation algorithms from the proofs, following Berger; the proofs are based on Tait-style reducibility predicates, and hence the extracted algorithms are instances of (weak head) normalization by evaluation, as already identified by Coquand and Dybjer. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1016/j.entcs.2005.11.056 | Electronic Notes in Theoretical Computer Science |
Keywords | DocType | Volume |
modified realizability,object language,first-order minimal logic,normal-order reduction,weak head normalization,evaluation algorithm,tait-style reducibility predicate,applicative-order reduction,program extraction,weak head,weak head normalization.,normalization by evaluation,first order | Journal | 155, |
ISSN | Citations | PageRank |
Electronic Notes in Theoretical Computer Science | 5 | 0.65 |
References | Authors | |
6 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Małgorzata Biernacka | 1 | 48 | 3.08 |
| Olivier Danvy | 2 | 1659 | 126.56 |
| Kristian Støvring | 3 | 64 | 6.91 |