Yes, I have! Girard is very… opinionated, he is fun to read for that reason. That is, Jean-Yves has some spicy takes:
Quantum logic is indeed a sort of punishment inflicted on nature, guilty of not yielding to the prejudices of logicians… just like Xerxes had the Hellespont – which had destroyed a boat bridge – whipped.
I enjoyed his book “Proofs and Types” as an introduction to type theory and the Curry-Howard correspondence. I’ve looked through “The Blind Spot” a bit and it also seemed like a fun read. Of course, you can’t avoid his name if you’re interested in linear logic (as I currently am), since the guy invented it.
Yes, I have! Girard is very… opinionated, he is fun to read for that reason. That is, Jean-Yves has some spicy takes:
I enjoyed his book “Proofs and Types” as an introduction to type theory and the Curry-Howard correspondence. I’ve looked through “The Blind Spot” a bit and it also seemed like a fun read. Of course, you can’t avoid his name if you’re interested in linear logic (as I currently am), since the guy invented it.