@article{DYBJER2012122,
    Abstract = {We prove the correctness of an algorithm for normalizing untyped combinator terms by evaluation. The algorithm is written in the functional programming language Haskell, and we prove that it lazily computes the combinatory B{\"o}hm tree of the term. The notion of combinatory B{\"o}hm tree is analogous to the usual notion of B{\"o}hm tree for the untyped lambda calculus. It is defined operationally by repeated head reduction of terms to head normal forms. We use formal neighbourhoods to characterize finite, partial information about data, and define a B{\"o}hm tree as a filter of such formal neighbourhoods. We also define formal topology style denotational semantics of a fragment of Haskell following Martin-L{\"o}f, and let each closed program denote a filter of formal neighbourhoods. We prove that the denotation of the output of our algorithm is the B{\"o}hm tree of the input term. The key construction in the proof is a ``glueing'' relation between terms and semantic neighbourhoods which is defined by induction on the latter. This relation is related to the glueing relation which was earlier used for proving the correctness of normalization by evaluation algorithm for typed combinatory logic.},
    Author = {Dybjer, Peter and Kuperberg, Denis},
    File = {Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation - 1-s2.0-S0168007211000972-main - a - k.pdf},
    ISSN = {0168-0072},
    Journal = {Annals of Pure and Applied Logic},
    Keywords = {Combinatory logic, Normalization by evaluation, Formal neighbourhoods, Lazy evaluation, B{\"o}hm trees},
    Note = {Third Workshop on Formal Topology},
    Number = {2},
    Pages = {122 - 131},
    Title = {Formal neighbourhoods, combinatory B{\"o}hm trees, and untyped normalization by evaluation},
    URL = {http://www.sciencedirect.com/science/article/pii/S0168007211000972},
    Volume = {163},
    Year = {2012},
    bdsk-url-1 = {http://www.sciencedirect.com/science/article/pii/S0168007211000972},
    bdsk-url-2 = {https://doi.org/10.1016/j.apal.2011.06.021},
    date-added = {2020-05-13 15:36:45 +0200},
    date-modified = {2020-05-13 15:36:45 +0200},
    doi = {10.1016/j.apal.2011.06.021}
}

@article{DYBJER2012122, Abstract = {We prove the correctness of an algorithm for normalizing untyped combinator terms by evaluation. The algorithm is written in the functional programming language Haskell, and we prove that it lazily computes the combinatory B{\"o}hm tree of the term. The notion of combinatory B{\"o}hm tree is analogous to the usual notion of B{\"o}hm tree for the untyped lambda calculus. It is defined operationally by repeated head reduction of terms to head normal forms. We use formal neighbourhoods to characterize finite, partial information about data, and define a B{\"o}hm tree as a filter of such formal neighbourhoods. We also define formal topology style denotational semantics of a fragment of Haskell following Martin-L{\"o}f, and let each closed program denote a filter of formal neighbourhoods. We prove that the denotation of the output of our algorithm is the B{\"o}hm tree of the input term. The key construction in the proof is a ``glueing'' relation between terms and semantic neighbourhoods which is defined by induction on the latter. This relation is related to the glueing relation which was earlier used for proving the correctness of normalization by evaluation algorithm for typed combinatory logic.}, Author = {Dybjer, Peter and Kuperberg, Denis}, File = {Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation - 1-s2.0-S0168007211000972-main - a - k.pdf}, ISSN = {0168-0072}, Journal = {Annals of Pure and Applied Logic}, Keywords = {Combinatory logic, Normalization by evaluation, Formal neighbourhoods, Lazy evaluation, B{\"o}hm trees}, Note = {Third Workshop on Formal Topology}, Number = {2}, Pages = {122 - 131}, Title = {Formal neighbourhoods, combinatory B{\"o}hm trees, and untyped normalization by evaluation}, URL = {http://www.sciencedirect.com/science/article/pii/S0168007211000972}, Volume = {163}, Year = {2012}, bdsk-url-1 = {http://www.sciencedirect.com/science/article/pii/S0168007211000972}, bdsk-url-2 = {https://doi.org/10.1016/j.apal.2011.06.021}, date-added = {2020-05-13 15:36:45 +0200}, date-modified = {2020-05-13 15:36:45 +0200}, doi = {10.1016/j.apal.2011.06.021} }