Sign in
Author

Conference

Journal

Organization

Year

DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all fields of study
Limit my searches in the following fields of study
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(1)
Strong Normalization
Related Publications
(2)
Lambdadefinabil...
Proving termination with Multiset Orderings
Subscribe
Academic
Publications
Proofs of strong normalization
Proofs of strong normalization,R. O. Gandy
Edit
Proofs of strong normalization
(
Citations: 37
)
BibTex

RIS

RefWorks
Download
R. O. Gandy
Published in 1980.
Cumulative
Annual
Citation Context
(21)
...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 Demangeon
,
et 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 Deng
,
et 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ørtz
,
et al.
Strong Normalization from Weak Normalization by Translation into the L...
...Examples can be found in Plotkin’s and Jung and Tiuryn’s lambdadefinability results using Irelations [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 Irelation [23], and Jung and Tiuryn’s proof that lambda terms satisfy any KLRwVA at each arity (Theorem 3 of [10])...
Furio Honsell
,
et al.
Prelogical Relations
Sort by:
Citations
(37)
Strong normalization property for second order linear logic
(
Citations: 5
)
Michele Pagani
,
Lorenzo Tortora De Falco
Journal:
Theoretical Computer Science  TCS
, vol. 411, no. 2, pp. 410444, 2010
Mobile Processes and Termination
(
Citations: 1
)
Romain Demangeon
,
Daniel Hirschkoff
,
Davide Sangiorgi
Conference:
Birthday ...
, pp. 250273, 2009
Termination Analysis of HigherOrder Functional Programs
(
Citations: 14
)
Damien Sereni
,
Neil D. Jones
Conference:
Asian Symposium on Programming Languages and Systems  APLAS
, pp. 281297, 2005
Probabilistic and Mobile Processes
Yuxin Deng
Published in 2005.
Ensuring Termination by Typability
(
Citations: 18
)
Yuxin Deng
,
Davide Sangiorgi
Conference:
IFIP International Conference on Theoretical Computer Science  IFIP TCS
, pp. 619632, 2004