Completeness of type assignment in continuous lambda models (Q792995)

The completeness of Curry's rules for assigning type schemes to terms of the pure lambda calculus is proved with respect to the model \(P_{\omega}\). An extension of Curry's system in which type schemes can be assigned to the fixed point combinator is introduced, together with a notion of type semantics, for which it is proved sound and complete. Also in this case completeness is proved with respect to the model \(P_{\omega}\).