Strong normalization from weak normalization in typed \(\lambda\)-calculi
type: Item
instance of: scholarly article
title: Strong normalization from weak normalization in typed \(\lambda\)-calculi
zbMATH Open document ID: 0878.03010
published in: Information and Computation
publication date: 1997-07-20T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 68Q42
zbMATH DE Number: 1022244
zbMATH Keywords: typed lambda-calculus
zbMATH Keywords: weak normalization
zbMATH Keywords: strong normalization
zbMATH Keywords: System F
author: M. H. B. Sørensen
describes a project that uses: Automath
MaRDI profile type: Publication
full work available at URL: inco.1996.2622
OpenAlex ID: W2044297003
cites work: Q4222771
cites work: The lambda calculus. Its syntax and semantics. Rev. ed.
cites work: Domain-free pure type systems
cites work: Q3674616
cites work: The Barendregt cube with definitions and generalised reduction
cites work: A-translation and looping combinators in pure type systems
cites work: Q5565113
cites work: Q4281472
cites work: A direct proof of the finite developments theorem
cites work: Q3994895
cites work: Corrigendum: Polymorphic type assignment and CPS conversion
cites work: Q4722037
cites work: Ordinal analysis of terms of finite type
cites work: A unified approach to type theory through a refined \(\lambda\)-calculus
cites work: Refining reduction in the lambda calculus
cites work: A useful \(\lambda\)-notation
cites work: Q3707989
cites work: Type reconstruction in finite rank fragments of the second-order \(\lambda\)-calculus
cites work: An analysis of ML typability
cites work: Q4501151
cites work: Q4942642
cites work: Combinatory reduction systems: Introduction and survey
cites work: Q4274979
cites work: Syntactic translations and provably recursive functions
cites work: Q3680263
cites work: Type inference with simple subtypes
cites work: Q3202991
cites work: Notions of computation and monads
cites work: Call-by-name, call-by-value and the \(\lambda\)-calculus
cites work: Q5559220
cites work: An equivalence between lambda- terms
cites work: Q3322086
cites work: An upper bound for reduction sequences in the typed \(\lambda\)-calculus
cites work: Q3922646
cites work: Effective longest and infinite reduction paths in untyped λ-calculi
cites work: Q4281487
cites work: Intensional interpretations of functionals of finite type I
cites work: Q4093416
cites work: Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
DOI: 10.1006/INCO.1996.2622
Recommended article: Q4501146
Recommended article: Computer Science Logic
Recommended article: Q3024920
Recommended article: Strong normalization from weak normalization by translation into the lambda-I-calculus
Recommended article: The Weak Normalization of the Simply Typed se-calculus
Recommended article: A formalization of strong normalization for simply-typed lambda-calculus and System F
Recommended article: Strong Normalisation in λ-Calculi with References
Recommended article: Strong normalizability of typed lambda-calculi for substructural logics
Recommended article: Strong normalisation for applied lambda calculi
Recommended article: Q5149155
description: scientific article; zbMATH DE number 1022244