Flavien Breuvart - On the characterization of models of H*: The semantical aspect

lmcs:1636 - Logical Methods in Computer Science, April 27, 2016, Volume 12, Issue 2 - https://doi.org/10.2168/LMCS-12(2:4)2016
On the characterization of models of H*: The semantical aspectArticle

Authors: 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 equational theory is H* (observations for head normalization). An extensional K-model $D$ is fully abstract if and only if it is hyperimmune, {\em i.e.}, not well founded chains of elements of D cannot be captured by any recursive function. This article, together with its companion paper, form the long version of [Bre14]. It is a standalone paper that presents a purely semantical proof of the result as opposed to its companion paper that presents an independent and purely syntactical proof of the same result.


    Volume: Volume 12, Issue 2
    Published on: April 27, 2016
    Submitted on: February 16, 2015
    Keywords: Computer Science - Logic in Computer Science,F.3.2

    Consultation statistics

    This page has been seen 1852 times.
    This article's PDF has been downloaded 420 times.