Doubly F-Bounded Generics

TL;DR

This paper introduces doubly f-bounded generics in object-oriented programming, extending existing concepts and providing a coinductive proof of the reasoning method's soundness.

Contribution

It proposes a new extension of f-bounded generics called doubly f-bounded generics and offers a coinductive approach to reason about them.

Findings

Extension of f-bounded generics to doubly f-bounded generics

A coinductive proof of the reasoning method's soundness

Framework for reasoning about complex generic bounds

Abstract

In this paper we suggest how f-bounded generics in nominally-typed OOP can be extended to the more general notion we call `doubly f-bounded generics' and we suggest how doubly f-bounded generics can be reasoned about. We also (attempt to) prove, using a coinductive argument, that our reasoning method is mathematically sound.