Finding a combination of types and static checks that guarantees some desired property such as type soundness (programms don’t get stuck) or consistency (not all types are inhabitated) is not enough. These checks should also be stable under those transformations that we perform when we write code. In “Deriving Dependently-Typed OOP from First Principles” that I will present at OOPSLA ’24, we extend the defunctionalization and refunctionalization transformations to dependent types, show that they are type preserving, and prove that the resulting system is sound. One of our major motivations is to allow programmers to switch between a functional design using data types and an object-oriented, interface-based design using codata types. However, the paper contains one major caveat: The system is not consistent since it doesn’t check for strict positivity of data and codata type declarations, uses the Type-in-Type axiom, and allows arbitrary mutual recursion. The reason we do not implement these checks is that although the defunctionalization and refunctionalization algorithms are semantics-preserving, the corresponding static checks are not preserved. For example, a program containing only strictly positive type declarations might be changed into a program in which type declarations contain negative recursive occurrances. This problem motivates the research problem that I am going to present: We want to find a way to check for the consistency of programs which is stable under defunctionalization and refunctionalization.