Girard's rhetoric never fails to keep me hooked. I treasure any number of works of Girard, whether his introductions to Type Theory and his Linear Logic or note

Girard's rhetoric never fails to keep me hooked. I treasure any number of works of Girard, whether his introductions to Type Theory and his Linear Logic or notes on his quest for Transcendental Logic. Clear prose of exposition, to the point and clearly motivated, intermingled with literary allusions in critique of philosophers' ideas of truth, the work of Girard is truly a gem. Particularly entertaining is his 'A pure waste of paper' (Appendix A of 'LOCUS SOLUM') (https://girard.perso.math.cnrs.fr/0.pdf https://girard.perso.math.cnrs.fr/0.pdf). I could flip to a random page of his 'appendix' and just sink in. A fine introductory work of his to the subject would be 'PROOFS AND TYPES' (https://people.mpi-sws.org/~dreyer/ats/papers/girard.pdf https://people.mpi-sws.org/~dreyer/ats/papers/girard.pdf).