Complete Types in an Extension of the System AF2
classification
🧮 math.LO
keywords
completereductionsystemtypesbetaexpansionextendextension
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.