Zobrazeno 1 - 3
of 3
pro vyhledávání: '"Peter Møller Neergaard"'
Publikováno v:
ICFP
Useful type inference must be faster than normalization. Otherwise, you could check safety conditions by running the program. We analyze the relationship between bounds on normalization and type inference. We show how the success of type inference is
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::53c540d3eca7018580b6009d25c2cbfe
https://doi.org/10.1145/1016848.1016871
https://doi.org/10.1145/1016848.1016871
Publikováno v:
Information and Computation. 178(1):149-179
For a notion of reduction in a λ-calculus one can ask whether a term satisfies conservation and uniform normalization. Conservation means that single-step reductions of the term preserve infinite reduction paths from the term. Uniform normalization
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::c135a2742d21044da210158bda52ce71
Autor:
Peter Møller Neergaard
Publikováno v:
Journal of Functional Programming. 15:669
This pearl gives a discount proof of the folklore theorem that every strongly $\beta$-normalizing $\lambda$-term is typable with an intersection type. (We consider typings that do not use the empty intersection $\omega$ which can type any term.) The
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::4fd25ca6444658f9f444489202f1f8f4
https://doi.org/10.1017/s0956796805005587
https://doi.org/10.1017/s0956796805005587