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 (13)

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

• 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
• 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

This page was built for publication: Strong normalization from weak normalization in typed \(\lambda\)-calculi