Complete Types in an Extension of the System AF2
Logic
2009-05-05 v1
Abstract
In this paper, we extend the system AF2 in order to have the subject reduction for the -reduction. We prove that the types with positive quantifiers are complete for models that are stable by weak-head expansion.
Keywords
Cite
@article{arxiv.0905.0371,
title = {Complete Types in an Extension of the System AF2},
author = {Samir Farkh and Karim Nour},
journal= {arXiv preprint arXiv:0905.0371},
year = {2009}
}