Recursive types and bounded quantification are prominent features in many modern programming languages, such as Java, C#, Scala or TypeScript. Unfortunately, the interaction between recursive types, bounded quantification and subtyping has shown to be problematic in the past. Consequently, defining a simple foundational calculus that combines those features and has desirable properties, such as \emph{decidability}, \emph{transitivity} of subtyping, \emph{conservativity} and a sound and complete algorithmic formulation has been a long time challenge.

This paper presents an extension of $\textrm{kernel}~F_{\le}$, called $F_{\le}^{\mu}$, with iso-recursive types. $F_\le$ is a well-known polymorphic calculus with bounded quantification. In $F_{\le}^{\mu}$ we add iso-recursive types, and correspondingly extend the subtyping relation with iso-recursive subtyping using the recently proposed nominal unfolding rules. We also add two smaller extensions to $F_\le$. The first one is a generalization of the $\textrm{kernel}~F_{\le}$ rule for bounded quantification that accepts \emph{equivalent} rather than \emph{equal} bounds. The second extension is the use of so-called \emph{structural} folding/unfolding rules, inspired by the structural unfolding rule proposed by Abadi, Cardelli, and Viswanathan [1996]. The structural rules add expressive power to the more conventional folding/unfolding rules in the literature, and they enable additional applications. We present several results, including: type soundness; transitivity and decidability of subtyping; the conservativity of $F_{\le}^{\mu}$ over $F_\le$; and a sound and complete algorithmic formulation of $F_{\le}^{\mu}$. Moreover, we study an extension of $F_{\le}^{\mu}$, called $F_{\le\ge}^{\mu}$, which includes \emph{lower bounded quantification} in addition to the conventional (upper) bounded quantification of $F_\le$. All the results in this paper have been formalized in the Coq theorem prover.