[TYPES] Typed lambda calculi with weak conversion

Filippo Sestini sestini.filippo at gmail.com
Sun Feb 25 06:06:46 EST 2018

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


[1] W.A. Howard, Assignment of Ordinals to Terms for Primitive
Recursive Functionals of Finite Type, 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

More information about the Types-list mailing list