An Infinitary Lambda Calculus with Global Trace Condition (Extended Abstract)

Stefano Berardi, Ugo de' Liguoro, Daisuke Kimura +1

We consider an extension of the infinitary lambda calculus by Kennaway et al., with zero, successor, and conditional, and a type system akin to Goedel's system T. For terms that ca…