TL;DR
This paper proves that I-types in System F, inhabited solely by I-terms, always contain a positive quantifier, and discusses implications and examples of this property.
Contribution
It establishes a new property of I-types in System F, showing they always include a positive quantifier, which was previously unknown.
Findings
I-types in System F have a positive quantifier.
Consequences of this property are explored.
Examples illustrating the result are provided.
Abstract
We prove in this paper that the types of system F inhabited uniquely by ?I-terms (the I-types) have a positive quantifier. We give also consequences of this result and some examples.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAdvanced Algebra and Logic · Advanced Topology and Set Theory · semigroups and automata theory