Recursive Types are prime examples for cylic objects occurring in Computer Science. Although algorithms for deciding, whether or not two recursive types are equivalent, have existed and been implemented in certain functional computer-languages for some time now, formal systems that allow the treatment of recursive type equivalence in a precise logical manner are fairly recent.
There are in particular (1) the axiomatization by R.~Amadio and L.~Cardelli (1993), (2) the axiomatization by M.~Brandt and F.~Henglein (1998) using a co-inductive derivation-rule, and (3) a syntactic matching inference-system as e.g. presented by Z.M.~Ariola and J.W.~Klop (1995), which can be used for consistency-testing of the equivalence of two given types.
In my talk I do want (a) to speak briefly about the motivation for recursive types in computer science, (b) to introduce the mentioned systems formally, (c) to give an example for a ``duality'' discovered by Prof.~Klop between derivations in the Brandt-Henglein-system and ``consistency checks'' in the syntactic-matching system and (d) to report shortly on which else proof-theoretic connections between these three kinds of systems I have found so far.