I will present a novel framework by Aaron Stump et al for a divide-and-conquer recursion scheme for a type theory similar to System F with subtyping that statically ensured termination just by usual type checking (in contrast to structural termination checking, which adds an additional termination checking step after type checking, and sized types, which augments the type theory with extra annotation specifically for the sake of termination checking). Previous work on this topic was published here. There is also ongoing work on a new programming language implementation based on D&C termination checking that I assisted with over the summer of 2025.