Alessio Guglielmi
Finally someone addresses my question about proof uniqueness! Google wasn't helping me at all, so I had to find it by accident.
Dan Sperber researches language, cognition, culture and evolution
...
My second research objective is to come up with useful, interesting notions of identity of proofs. It is embarrassing for proof theory that the natural question of `when are two proofs to be considered identical?ยด lacks good answers.* (This question is tightly connected to the equally non-well-understood problem of deciding when two algorithms are the same.) One reason for our embarrassment is that the notion of normalisation available, viz. cut elimination, is inadequate to decide the question; I believe that the problem is that this is the only (reasonable) normalisation notion available in the sequent calculus and natural deduction. Thanks to its finer granularity, the calculus of structures offers several natural new notions of normalisation, this way improving our ability to study new concepts of identity.
...
Finally someone addresses my question about proof uniqueness! Google wasn't helping me at all, so I had to find it by accident.
Dan Sperber researches language, cognition, culture and evolution