Derivation Lengths Classification of G\"odel's T Extending Howard's Assignment

DOI10.2168/LMCS-8(1:19)2012zbMath1238.03025arXiv1203.0115OpenAlexW2036716130MaRDI QIDQ2881086

Andreas Weiermann, Gunnar Wilken

Publication date: 3 April 2012

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1203.0115

zbMATH Keywords

rewrite systemterminationstrong normalizationtyped \(\lambda \)-calculusGödel's T

Mathematics Subject Classification ID

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

Related Items (3)

Gentzen's consistency proof without heightlines ⋮ Size-based termination of higher-order rewriting ⋮ A Glimpse of $$ \sum_{3} $$-elementarity

This page was built for publication: Derivation Lengths Classification of G\"odel's T Extending Howard's Assignment