[TYPES] Typed lambda calculi with weak conversion

[Filippo Sestini]

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
sestini.filippo at gmail.com
(+39) 333 6757668