Complete Types in an Extension of the System AF2

TL;DR

This paper extends the AF2 type system to ensure subject reduction for beta-eta reduction and proves completeness of positive quantifier types for certain models.

Contribution

It introduces an extension to AF2 that guarantees subject reduction and establishes completeness results for positive quantifier types.

Findings

Types with positive quantifiers are complete for models stable under weak-head expansion.

The extended AF2 system maintains subject reduction for beta-eta reduction.

Theoretical proof of completeness for a class of models.

Abstract

In this paper, we extend the system AF2 in order to have the subject reduction for the $\beta\eta$-reduction. We prove that the types with positive quantifiers are complete for models that are stable by weak-head expansion.