Inductively defined types. - Thierry Coquand; Christine Paulin (Conference on Computer Logic, 1988)