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

DOI10.1016/J.APAL.2004.10.003MaRDI QIDQ1772771zbMATH OpenOpenAlexFDO

Authors Klaus Aehlig, Felix Joachimski

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\)-calculus\(\omega\)-ruleContinuous normalizationCut elimination and \(\beta\)-reductionsLength of reduction sequenceSize of normal formBöhm treesGödel's T

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1948154
• Non-determinism, non-termination and the strong normalization of System T
• New Computational Paradigms
• Strong normalisation for applied lambda calculi
• Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)

Cites work

• scientific article; zbMATH DE number 1615235 (Why is no real title available?)
• scientific article; zbMATH DE number 3933067 (Why is no real title available?)
• scientific article; zbMATH DE number 3497842 (Why is no real title available?)
• scientific article; zbMATH DE number 3508467 (Why is no real title available?)
• scientific article; zbMATH DE number 3572133 (Why is no real title available?)
• scientific article; zbMATH DE number 1948154 (Why is no real title available?)
• scientific article; zbMATH DE number 1797606 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• A proof of strongly uniform termination for Gödel's \(T\) by methods from local predicativity
• Analyzing Gödel's T Via Expanded Head Reduction Trees
• Beweistheoretische Erfassung der unendlichen Induktion in der Zahlentheorie
• Confluence of the coinductive \(\lambda\)-calculus
• Exact bounds for lengths of reductions in typed \(\lambda\)-calculus
• Finite investigations of transfinite derivations
• Finite notations for infinite terms
• Notation systems for infinitary derivations
• Perpetual reductions in -calculus
• Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
• Universal coalgebra: A theory of systems
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES

Cited in

(6)

• scientific article; zbMATH DE number 1948154 (Why is no real title available?)
• scientific article; zbMATH DE number 4068861 (Why is no real title available?)
• Analyzing Gödel's T Via Expanded Head Reduction Trees
• Typed Lambda Calculi and Applications
• scientific article; zbMATH DE number 1223615 (Why is no real title available?)
• On the computational complexity of cut-reduction

This page was built for publication: Continuous normalization for the lambda-calculus and Gödel's T

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1772771)