This work gives the first decidability results on type isomorphism for recursive types, establishing the explicit decidability of type isomorphism for the type theory of sums and products over an inhabited generic recursive polynomial type.
The technical development also gives the first connection between themes in programming language theory (type isomorphism) and computational algebra (Grobner bases).
