Proofs and Types

by Jean-Yves Girard, Yves LaFont, Paul Taylor

This text is an outgrowth of notes prepared by J.-Y. Girard for a course at the University of Paris VII. It deals with the mathematical background of the application to computer science of aspects of logic (namely the correspondence between proposition and types). Combined with the conceptual perspectives of Girard's ideas, this sheds light on both the traditional logic material and its prospective applications to computer science. The book covers a very active and exciting research area, and it will be essential reading for all those working in logic and computer science.

Genres: Mathematics, Logic, Computer Science, Philosophy, Programming

192 pages, Hardcover

First published April 28, 1989

About the author

Jean-Yves Girard (born 1947) is a French logician working in proof theory. His contributions include a proof of strong normalization in a system of second-order logic called system F; the invention of linear logic; the geometry of interaction; and ludics. He also invented the mustard watch.

Alumnus of the École normale supérieure de Saint-Cloud, Girard is a research director of CNRS in Marseille and a corresponding member of the French Academy of Sciences.

Reviews

[Carter · Rating 3 out of 5]

I was a bit disappointed by this book. It states general results in outline, but omits the proofs.