To insert individual citation into a bibliography in a word-processor,
select your preferred citation style below and drag-and-drop it into the document.
Electronic Notes in Theoretical Computer Science, Vol. 155 (May 2006), pp. 169-189, doi:10.1016/j.entcs.2005.11.056 Key: citeulike:11263566
Formatted Citation
Show HTML
Likes
(beta)
This copy of the article hasn't been liked by anyone yet.
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.
CiteULike organises scholarly (or academic) papers or literature and provides bibliographic
(which means it makes bibliographies) for universities and higher education establishments.
It helps undergraduates and postgraduates. People studying for PhDs or in postdoctoral (postdoc) positions.
The service is similar in scope to EndNote or RefWorks or any other reference manager
like BibTeX, but it is a social bookmarking service for scientists and humanities researchers.
There are no reviews yet
