Academic
Publications
Proofs of strong normalization

Proofs of strong normalization,R. O. Gandy

Proofs of strong normalization   (Citations: 37)
BibTex | RIS | RefWorks Download
Published in 1980.
Cumulative Annual
    • ...In computer science, termination has been extensively investigated in term rewriting systems [DM79, DH95] and λcalculi [Gan80, Mit96], where strong normalization is a more commonly used synonym...

    Romain Demangeonet al. Mobile Processes and Termination

    • ...In computer science termination has been extensively investigated in term rewriting systems [7, 5] and -calculi [9, 4] (where strong normalization is a synonym more commonly used)...

    Yuxin Denget al. Ensuring Termination by Typability

    • ...The reducibility argument usually used for this proof can not be carried out in Primitive Recursive Arithmetic (PRA ), while strong normalization for natural deduction can, like in [Gir87] . This proof of [Gir87] reduces strong normalization to weak normalization by PRA means — following the argument that [Gan80] introduced for Go ¨del’s system . In the ND case the proof of weak normalization is clearly a proof of PRA , and therefore ...

    Projet MEIJE. A note on intersection types

    • ...• In Gandy’s [4] proof of strong normalization for simply typed λ-calculus...
    • ...Next (Section 5) we study Gandy’s translation [4]...
    • ...Gandy [4] studies a translation · ∗ from � → to � → I followed by an interpretation [[·]] into monotone functionals over the natural numbers...
    • ...Remark. The above definition of · ∗ is due to van de Pol [16]. Gandy’s [4] definition is...

    Inge Li Gørtzet al. Strong Normalization from Weak Normalization by Translation into the L...

    • ...Examples can be found in Plotkin’s and Jung and Tiuryn’s lambda-definability results using I-relations [23] and Kripke logical relations with varying arity [10] respectively, and Gandy’s proof of strong normalization using hereditarily strict monotonic functionals [6]...
    • ...Gandy’s hereditarily strict monotonic functionals [6] can be defined using the above technique with just a small modification of the clause for functionals...
    • ...Examples include Gandy’s proof that the hereditarily strict monotonic functionals model �I terms [6], Plotkin’s proof that lambda terms satisfy any I-relation [23], and Jung and Tiuryn’s proof that lambda terms satisfy any KLRwVA at each arity (Theorem 3 of [10])...

    Furio Honsellet al. Prelogical Relations

Sort by: