Recursive Types are prime examples for cylic objects occurring in Computer Science. Although algorithms for deciding, whether or not two recursive types are either equivalent or in the subtype-relation, have existed for quite some time now, formal systems that allow the formal treatment of the equality and subtype-relations between recursive types in a precise logical manner are fairly recent.
For both these relations there are in particular three different kinds of formal proof-systems: (1) The axiomatizations by R. Amadio and L. Cardelli (1993), (2) the axiomatizations by M. Brandt and F. Henglein (1998), which each contain a co-inductive derivation-rule, and (3) the so called syntactic-matching inference-systems as e.g. presented and applied (in a slightly different setting) by Z.M. Ariola and J.W. Klop (1995), which systems can be used for consistency-checking of formal statements, that assert that the r.t.-equality or, respectively, that the r.t.-subtyping relation holds for two given recursive types.
After speaking briefly about the motivation for recursive types in Computer Science I do want (a) to give the precise definitions of the notions of "recursive type equality" (also called r.t."-equivalence") and of the "subtyping relation between recursive types", (b) to introduce formally the systems mentioned above, (c) to motivate by the use of an example a ``duality'' discovered by J.W. Klop between derivations in a variant-Brandt-Henglein-system and ``consistency checks'' in a respective syntactic-matching system, (d) to sketch proof-theoretic transformations between derivations in the respective Amadio-Cardelli- and derivations in the respective Brandt-Henglein-systems, (e) to point at and discuss some side-issues and (f) to report on a perhaps previously unnoticed direct connection between the Amadio-Cardelli- and the Brandt-Henglein-systems in the case of the subtyping relation.
