Axioms for Definability and Full Completeness
Logic in Computer Science
2014-01-22 v2
Abstract
Axioms are presented which encapsulate the properties satisfied by categories of games which form the basis of results on full abstraction for PCF and other programming languages, and on full completeness for various logics and type theories. Axioms are presented on models of PCF from which full abstraction can be proved. These axioms have been distilled from recent results on definability and full abstraction of game semantics for a number of programming languages. Full completeness for pure simply-typed -calculus is also axiomatized.
Cite
@article{arxiv.1401.4735,
title = {Axioms for Definability and Full Completeness},
author = {Samson Abramsky},
journal= {arXiv preprint arXiv:1401.4735},
year = {2014}
}
Comments
18 pages