[TYPES] Typed lambda calculi with weak conversion
t.altenkirch at googlemail.com
Thu Mar 1 07:15:27 EST 2018
you can define weak equality using a substitution calculus. The basic idea is that you have normal forms of the form (\x.t)[us and laws like ((\x.t)[us])[vs] = (\x.t)[us o vs], see http://www.cs.nott.ac.uk/~psztxa/publ/jtait07.pdf, p.6.
On 25/02/2018, 11:06, "Types-list on behalf of Filippo Sestini" <types-list-bounces at LISTS.SEAS.UPENN.EDU on behalf of sestini.filippo at gmail.com> wrote:
>[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>The notion of weak reduction first appeared in , and was later
>developed into the definition of a weak lambda calculus in, for
>example, . 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 (, ).
>Do you have any suggestions?
> W.A. Howard, Assignment of Ordinals to Terms for Primitive
>Recursive Functionals of Finite Type, 1970
> N. Çağman, J.R. Hindley, Combinatory weak reduction in lambda
> P. Martin-Löf, An Intuitionistic Theory of Types: Predicative
> T. Coquand, P. Dybjer, Intuitionistic Model Constructions and
>Normalization Proofs, 1998
>sestini.filippo at gmail.com
>(+39) 333 6757668
More information about the Types-list