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

lmcs:1636 - Logical Methods in Computer Science, April 27, 2016, Volume 12, Issue 2
On the characterization of models of H*: The semantical aspect

Authors: Breuvart, Flavien

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.


Source : oai:arXiv.org:1603.07259
DOI : 10.2168/LMCS-12(2:4)2016
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


Share

Consultation statistics

This page has been seen 93 times.
This article's PDF has been downloaded 59 times.