Portal de Periódicos da CAPES

Higman's lemma in type theory

1998; Springer Science+Business Media; Linguagem: Inglês

10.1007/bfb0097789

1611-3349

Daniel Fridlender,

Geometric and Algebraic Topology

This paper starts with a brief exploration of the history of Higman's lemma with emphasis on Veldman's recent intuitionistic proof, which established the lemma in its most general form. The rest of the paper is devoted to the description of a type-theoretic proof of such a general form of Higman's lemma. This involves considering type-theoretic formulations of bar induction, fan theorem, Ramsey theorem, and Higman's lemma. The proof was formalized in Martin-Löf's type theory without universes, and edited and checked in the proof editor ALF.