Ramsey's theorem in type theory
| Author(s) : | Daniel Fridlender, |
| Publisher : | N/A |
| Publication Date : | 1993 |
| ISSN : | N/A |
| Abstract : | We present formalizations of constructive proofs of the Intuitionistic Ramsey Theorem and Higman's Lemma in Martin-Lof's Type Theory. We analyze the computational content of these proofs and we compare it with programs, |