Computer Science Department

Computer Science Colloquium

From Frege to Gosling:19'th century logic and 21'st century programming languages

Philip Wadler
Avaya Labs

Monday, April 21, 2003 (Postponed from April 7)
11:00 a.m.
Room 1302 WWH
251 Mercer Street
New York, NY 10012-1185

Host: Richard Cole,, 212-998-3119
Colloquium Information:


Logics of the 19'th century, developed by philosophers like Gottlieb Frege concerned with the nature of truth, have direct impact on programming languages for the 21'st century, designed by engineers like James Gosling concerned with programming the web. The type systems developed by logicians underlie the safety properties of Java that make exchange of programs possible. One of the most fascinating tales of the 20'th century is how Gentzen's natural deduction (a model of logic) and Church's lambda calculus (a model of programming) were discovered, a half century after their invention, to be in precise correspondence. One aspect of the correspondence is an association between second-order quantification and generic types. The talk describes GJ, which is based on this correspondence, and serves as the basis of Sun's plans to add generics to Java. The talk also describes Featherweight Java, a model of Java that is comparable in simplicity and power to lambda calculus, and serves as a tool for designing the generation of languages to follow Java.

Based on work with Martin Odersky, Gilad Bracha, David Stoutamire, Benjamin Pierce, and Atsushi Igarashi.)