Perpetual reductions in \(\lambda\)-calculus
type: Item
instance of: scholarly article
title: Perpetual reductions in \(\lambda\)-calculus
zbMATH Open document ID: 0920.03024
author: Femke van Raamsdonk
author: M. H. B. Sørensen
author: Hongwei Xi
author: Paula Severi
published in: Information and Computation
publication date: 1999-09-09T00:00:00Z
Mathematics Subject Classification ID: 03B40
zbMATH DE Number: 1283689
zbMATH Keywords: \(\beta\)-reduction
zbMATH Keywords: \(\lambda\)-calculus
zbMATH Keywords: perpetual reductions
zbMATH Keywords: perpetual redexes
zbMATH Keywords: infinite reduction paths
zbMATH Keywords: survey
zbMATH Keywords: type theory
describes a project that uses: Automath
MaRDI profile type: Publication
full work available at URL: inco.1998.2750
OpenAlex ID: W2130554190
cites work: Q4023900
cites work: The lambda calculus. Its syntax and semantics. Rev. ed.
cites work: Needed reduction and spine strategies for the lambda calculus
cites work: Church-Rosser strategies in the lambda calculus
cites work: Q3674616
cites work: Q4133598
cites work: A general method for proving the normalization theorem for first and second order typed λ-calculi
cites work: Some Properties of Conversion
cites work: Q5565113
cites work: Q4501144
cites work: On termination and confluence properties of disjoint and constructor-sharing conditional rewrite systems
cites work: Reductions of Residuals are Finite
cites work: BCK-combinators and linear \(\lambda\)-terms have types
cites work: Q4722037
cites work: Q4260372
cites work: Ordinal analysis of terms of finite type
cites work: Q3707989
cites work: Optimal normalization in orthogonal term rewriting systems
cites work: Q4501151
cites work: Q4954449
cites work: Discrete Normalization and Standardization in Deterministic Residual Structures
cites work: Q4364379
cites work: Q3918095
cites work: Q4274979
cites work: Lambda-calculus terms that reduce to themselves
cites work: The Standardization Theorem for λ‐Calculus
cites work: Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
cites work: Finite family developments
cites work: Q3976042
cites work: Polynomial time termination and constraint satisfaction tests
cites work: Q3127078
cites work: Q3024848
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: Q4880706
cites work: Effective longest and infinite reduction paths in untyped λ-calculi
cites work: Q4511325
cites work: Strong normalization from weak normalization in typed \(\lambda\)-calculi
cites work: A Note on Shortest Developments
cites work: Intensional interpretations of functionals of finite type I
cites work: Parallel reductions in \(\lambda\)-calculus
cites work: Reduction of higher type levels by means of an ordinal analysis of finite terms
cites work: Strong normalization in type systems: A model theoretical approach
cites work: A direct proof of the finite developments theorem
cites work: Q3783265
cites work: Q3024920
DOI: 10.1006/INCO.1998.2750
description: scientific article; zbMATH DE number 1283689