Sciweavers

LFCS
1994
Springer
14 years 3 months ago
Strong Normalization in a Non-Deterministic Typed Lambda-Calculus
In a previous paper [4], we introduced a non-deterministic -calculus (-LK) whose type system corresponds exactly to Gentzen's cut-free LK [9]. This calculus, however, cannot b...
Philippe de Groote