tag:blogger.com,1999:blog-11295132.post114247119943879584..comments2014-04-16T10:57:46.206-07:00Comments on A Neighborhood of Infinity: Homotopies between proofs and between programsDan Piponihttps://plus.google.com/107913314994758123748noreply@blogger.comBlogger3125tag:blogger.com,1999:blog-11295132.post-1143716997086362492006-03-30T03:09:00.000-08:002006-03-30T03:09:00.000-08:00Normalisation of proofs in Natural Deduction has b...Normalisation of proofs in Natural Deduction has been shown to be related to finding normal forms of lambda terms via the howard-curry correspondance. I imagine that finding equivelent lambda terms is closely related to homotopies of proofs.Jacobianhttp://www.blogger.com/profile/03650584449231540008noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-1142522829752975962006-03-16T07:27:00.000-08:002006-03-16T07:27:00.000-08:00I'm busy giving myself a crash course in category ...I'm busy giving myself a crash course in category theory at the moment. Though I studied algebraic topology years ago I never did category theory for its own sake. Among other things I'm wondering about some down to earth stuff - using linear logic to do linear mathematics. Eg. linear types allow you to do matrix and vector operations more efficiently in place.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-1142495679436467152006-03-15T23:54:00.000-08:002006-03-15T23:54:00.000-08:00Jon Cohen (http://thatlogicblog.blogspot.com) was ...Jon Cohen (http://thatlogicblog.blogspot.com) was trying to teach me about cartesian closed categories and refresh my memory about homotopies enough to help him come up with such a topology, when I was in Australia last year. He's very sharp, and seems good at motivating people, so I wouldn't be surprised if he's got some more relevant stuff by now.Kennyhttp://www.blogger.com/profile/12226268498253877151noreply@blogger.com