Strong normalization from weak normalization in typed \(\lambda\)-calculi

DOI10.1006/inco.1996.2622zbMath0878.03010OpenAlexW2044297003MaRDI QIDQ1357009

Morten Heine B. Sørensen

Publication date: 20 July 1997

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1006/inco.1996.2622

zbMATH Keywords

weak normalizationstrong normalizationtyped lambda-calculusSystem F

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40)

Related Items

Resource operators for \(\lambda\)-calculus, The conservation theorem for differential nets, On strong normalization and type inference in the intersection type discipline, De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: The typed case, De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: the untyped case, Weak normalization implies strong normalization in a class of non-dependent pure type systems, On the longest perpetual reductions in orthogonal expression reduction systems, Strong cut-elimination in sequent calculus using Klop's ι-translation and perpetual reductions, Strong Normalisation of Cut-Elimination That Simulates β-Reduction, Perpetual reductions in \(\lambda\)-calculus, Strong normalization property for second order linear logic, Perpetuality and uniform normalization in orthogonal rewrite systems, Conservation and uniform normalization in lambda calculi with erasing reductions

Uses Software

• Automath

Cites Work

• Notions of computation and monads
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Type reconstruction in finite rank fragments of the second-order \(\lambda\)-calculus
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Combinatory reduction systems: Introduction and survey
• An equivalence between lambda- terms
• A unified approach to type theory through a refined \(\lambda\)-calculus
• A useful \(\lambda\)-notation
• Corrigendum: Polymorphic type assignment and CPS conversion
• The Barendregt cube with definitions and generalised reduction
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• An upper bound for reduction sequences in the typed \(\lambda\)-calculus
• Syntactic translations and provably recursive functions
• A direct proof of the finite developments theorem
• Ordinal analysis of terms of finite type
• An analysis of ML typability
• Domain-free pure type systems
• A-translation and looping combinators in pure type systems
• Refining reduction in the lambda calculus
• Type inference with simple subtypes
• Intensional interpretations of functionals of finite type I
• Effective longest and infinite reduction paths in untyped λ-calculi
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item