Greedy Implicit Bounded Quantification in Object-Oriented Programming Languages

Explore a groundbreaking 18-minute video presentation from OOPSLA2 2023 on Greedy Implicit Bounded Quantification. Delve into the innovative research by Chen Cui, Shengyi Jiang, and Bruno C. d. S. Oliveira from the University of Hong Kong, addressing the challenges of type-inference algorithms for bounded quantification in object-oriented programming languages. Learn about their novel variant of kernel F≤, called F≤b, which offers both declarative and algorithmic formulations of the type system. Discover how this approach enables implicit polymorphism with fewer type annotations, while maintaining compatibility with explicit type applications for impredicative instantiations. Gain insights into the completeness result with respect to kernel F≤ and the mechanically formalized proofs using the Abella theorem prover. Access supplementary materials, including reusable artifacts, to further enhance your understanding of this significant contribution to type system research.