Inductively defined types. - Coquand, Thierry; Paulin, Christine (1988)