Abstract:
This report identifies a general method for defining mutually-recursive concrete types and deriving their abstract axiomatisations in higher-order logic. The method is designed to preserve consistency and is tailored to the implementation of an efficient, automated type definition facility for the interactive theorem prover HOL90.
Edinburgh, 4th Year Undergraduate Project Report, 1992.
This is a 59-page article. It is available in the following forms.