tag:blogger.com,1999:blog-11295132.post114247119943879584..comments2024-02-24T01:46:31.188-08:00Comments on A Neighborhood of Infinity: Homotopies between proofs and between programssigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comBlogger2125tag: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.Gavin Mendel-Gleasonhttps://www.blogger.com/profile/14899896537888421449noreply@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.sigfpehttps://www.blogger.com/profile/08096190433222340957noreply@blogger.com