Continuous normalization for the lambda-calculus and Gödel's T

DOI10.1016/j.apal.2004.10.003zbMath1066.03055OpenAlexW2024515723MaRDI QIDQ1772771

Felix Joachimski, Klaus Aehlig

Publication date: 21 April 2005

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.apal.2004.10.003

zbMATH Keywords

\(\lambda\)-calculusBöhm treesGödel's T\(\omega\)-ruleContinuous normalizationCut elimination and \(\beta\)-reductionsLength of reduction sequenceSize of normal form

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Combinatory logic and lambda calculus (03B40)

Related Items

On the computational complexity of cut-reduction

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Finite investigations of transfinite derivations
• Perpetual reductions in \(\lambda\)-calculus
• Finite notations for infinite terms
• A proof of strongly uniform termination for Gödel's \(T\) by methods from local predicativity
• Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
• Universal coalgebra: A theory of systems
• Confluence of the coinductive \(\lambda\)-calculus
• Notation systems for infinitary derivations
• Beweistheoretische Erfassung der unendlichen Induktion in der Zahlentheorie
• Exact bounds for lengths of reductions in typed λ-calculus
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Analyzing Gödel's T Via Expanded Head Reduction Trees