arXiv · 0905.0371
Complete Types in an Extension of the System AF2
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.
Explore related subjects
Keep this discovery
Samir Farkh, Karim Nour. 2009-05-04. Complete Types in an Extension of the System AF2. https://arxiv.org/abs/0905.0371
Cite the original work for its findings. Save a collection to share your selection of sources.