Submitted by Paweł Urzyczyn

Date: 1993

Statement. Are there terms untypable in but typable with help of positive
recursive types?

[PRINT this PROBLEM]

Consider an extension of simply typed lambda-calculus obtained by adding the construct for types containing only positive occurrences of , together with the rules:

[Urzyczyn, 1996] Urzyczyn, P. (1996). Positive recursive type assignment. Fundamenta Informaticae, 28(1-2):197–209.

[Urzyczyn, 1997] Urzyczyn, P. (1997). Type reconstruction in . Mathematical Structures in Computer Science, 7(4):329–358.

[Next] [Previous] [Up]

Last modified: July 21, 2014