Normal forms in the typed lambda-calculus with tuple types.
Jiří Zlatuška · Czech digital mathematics library · 1985
JIRf ZLATUSKAA modified typed A-calculus with types containing, in addition to function types, also product types is studied.A notion of reduction, including bijective tuple and projection operations, is introduced and it is shown that it is both strongly normalizing and Church-Rosser.