Inductively defined types - Thierry Coquand; Christine Paulin (COLOG-88, International Conference on Computer Logic, Tallinn, USSR, December 1988, Proceedings, 1988)