Jean Yves Girard

Mathematician. "Founding father" of LinearLogic. Home page at http://iml.univ-mrs.fr/~girard/

Articles on the subject of LinearLogic at http://iml.univ-mrs.fr/~girard/Articles.html

See: JeanYvesGirardOnGoedelEscherBach, GirardLecturesOnProofTheory

Jean Yves Girard has a marvelous writing skill. Here's an example

According to Herodotus (VII,35), a tempest destroyed the military bridges built by Xerxes over the Hellespont ; he decided to punish nature and to have the sea whipped. To some extent, this is what logicians wanted to do to quantum physics, to punish it for being "against common-sense". Among the untold things was surely the idea of a complete schizophrenia between nature and spirit : our beautiful minds were harboured by the wrong world and this was a mere accident. The logical accounts of quantum phenomena were contrived on purpose, as in the notorious quantum logic ; the subliminal message being : "quantum or not, just a matter of encoding".

: from "Between logic and quantic : a tract"
: http://iml.univ-mrs.fr/~girard/LLcup.pdf.gz

For people passionate of math, logic and their relation to programming there's good news. Recently his book, ProofsAndTypes, has been made available online:

http://www.cs.man.ac.uk/~pt/stable/Proofs+Types.html

Another very nice text recently put online are his book on ProofTheory based on his course at Roma:

http://iml.univ-mrs.fr/~girard/coursang/coursang.html (in english)

It is also available in french, and will soon be published at Hermann in two volumes format.

Even if one knows the subject matters from an university course or another book, reading Girard offers something unique: it's not just dry math, it's perspective + insight + humor + style + dry math. Among the many insights to be found in Girard's writing is his re-evaluation of the evolution of logic and meta-mathematics. All philosophic speculations on the implications of the technical results in meta-mathematics are subjected to a healthy doze of ridicule. Girard allows the reader to look at logic with fresh new eyes.

I'm passionate on the above ("math, logic and their relation to programming"), however, I've studied meta-mathematics more than casually, and LinearLogic via e.g. HenryBaker; what will I learn if I read ProofsAndTypes? He may be a great writer, but I have to allocate my readings to optimize cost/benefit.

CategoryAuthor