[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Dear all, The notion of weak reduction first appeared in [1], and was later developed into the definition of a weak lambda calculus in, for example, [2]. The crucial property of weak reduction is that it does not validate the ξ rule, but some form of computation under binders is still possible. I'm looking for references in the literature treating typed calculi with full lambda syntax and weak conversion, in particular regarding normalization. What I've found so far seems to either be limited to a form of combinator syntax, or only consider evaluation to weak head normal form ([3], [4]). Do you have any suggestions? Thank you Sincerely [1] W.A. Howard, Assignment of Ordinals to Terms for Primitive Recursive Functionals of Finite Type, 1970 1970 [2] N. Çağman, J.R. Hindley, Combinatory weak reduction in lambda calculus, 1998 [3] P. Martin-Löf, An Intuitionistic Theory of Types: Predicative Part, 1975 [4] T. Coquand, P. Dybjer, Intuitionistic Model Constructions and Normalization Proofs, 1998 -- Filippo Sestini [email protected] (+39) 333 6757668
