Syntactic Considerations on Recursive Types

           Martin Abadi                 Marcelo P. Fiore     

          ma@pa.dec.com                 mf@dcs.ed.ac.uk
     Systems Research Center                  LFCS
  Digital Equipment Corporation      University of Edinburgh

                           Abstract

We study recursive types from a syntactic perspective.  In particular,
we compare the formulations of recursive types that are used in
programming languages and formal systems.  Our main tool is a new
syntactic explanation of type expressions as functors.  We also
introduce a simple logic for programs with recursive types in which
we carry out our proofs.