Strong normalization from weak normalization in typed \(\lambda\)-calculi (Q1357009)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
scientific article; zbMATH DE number 1022244
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Strong normalization from weak normalization in typed \(\lambda\)-calculi |
scientific article; zbMATH DE number 1022244 |
Statements
Strong normalization from weak normalization in typed \(\lambda\)-calculi (English)
0 references
20 July 1997
0 references
For some typed \(\lambda\)-calculi it is easier to prove weak normalization than strong normalization. Techniques to infer the latter from the former have been invented but they infer strong normalization of one notion of reduction from weak normalization of a more complicated notion of reduction. The paper presents a new technique to infer strong normalization from weak normalization of the same notion of reduction. This is demonstrated by examples including System F.
0 references
typed lambda-calculus
0 references
weak normalization
0 references
strong normalization
0 references
System F
0 references
0 references
0.9498596
0 references
0.94084203
0 references
0.93013644
0 references
0.92959297
0 references
0.92820275
0 references
0.9277985
0 references
