Coinductive Axiomatization of Recursive Type Equality and Subtyping
Michael Brandt, Fritz Henglein · Fundamenta Informaticae · 1998
We present new sound and complete axiomatizations of type equality and subtype inequality for a first-order type language with regular recursive types. The rules are motivated by coinductive characterizations of type containment and type equality via