On the characterization of models of H*: The semantical aspect

Flavien Breuvart

We give a characterization, with respect to a large class of models of untyped lambda-calculus, of those models that are fully abstract for head-normalization, i.e., whose equation…