Qualifying System F-sub
summary
Paper claims a practical calculus System F<:Q that combines higher‑rank bounded polymorphism with a free lattice encoding of qualifier expressions, giving concrete subqualification rules and bounded qualifier variables. It adds runtime constructs (asserts and upcasts) so progress and preservation hold and proves safety properties: e.g. immutability prevents writes through const references and a function‑coloring scheme ensures red functions never call blue ones. This is theory only; an implementation is in progress.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:56Type qualifiers lattice
- 3:29Polymorphism challenge
- 5:54Free lattice construction
- 8:22System F-sub with qualifiers
- 9:47Reference immutability
- 11:10Function coloring case study
- 12:35Related qualifier systems
- 14:41Takeaways and future work
- 15:25Q&A
related talks
15mQualified Types with Boolean Algebras
15mSimple Reference Immutability for System F-sub
16mTowards formally secure compilation of verified F* programs against unverified ML(…)
19mTowards Tagless Interpretation of Stratified System F (Extended Abstract)
32mVerifying Haskell's Rewrite Rules based on Polymorphic Rewriting Theory
19mExtensible Metatheory Mechanization via Family Polymorphism
16mInterpolation and Quantifiers in Ortholattices
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)