isomorphisms of generic recursive polynomial types
This paper 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 provides connections between themes in programming-language theory (type isomorphism) and computational algebra (Grbner bases).
type isomorphism recursive types type theory word problem semigroups rigs gr&#246 bner bases data structure