RECURSIVE MODELS OF GENERAL INDUCTIVE TYPES

Article type: Research Article

Authors: Fu, Yuxi

Affiliations: Department of Computer Science, University of Manchester M13 9PL, England

Note: [] During the preparation of this paper, the author was supported by the CLICS-II project. In the later stage of the preparation, he was under the 863 Project.

Note: [] Author's present address: Department of Computer Science, Shanghai Jiao Tong University, 1954 Hua Shan Road, Shanghai 200030, People's Republic of China.

Abstract: We give an interpretation of Martin-Löf's type theory (with universes) extended with generalized inductive types. The model is an extension of the recursive model given by Beeson. By restricting our attention to PER model, we show that the strictness of positivity condition in the definition of generalized inductive types can be dropped. It therefore gives an interpretation of general inductive types in Martin-Löf's type theory.

DOI: 10.3233/FI-1996-26202

Journal: Fundamenta Informaticae, vol. 26, no. 2, pp. 115-131, 1996