Functional Encodings of Mathematics (T: 45 min + Q: 15min)

Jun 15, 2022, 1:30 PM
Centre de conférences Marilyn et James Simons (Le Bois-Marie)

Centre de conférences Marilyn et James Simons

Le Bois-Marie

35, route de Chartres 91440 Bures-sur-Yvette


Prof. Georges GONTHIER (INRIA)


A remarkable feature of logics based on typed lambda calculus is that they allow embedding functional programs in the representation of mathematical knowledge.
These can be used to animate formal theories and make them behave, in part, as a working mathematician would expect. Examples of such functional encodings have played a key part in several large formal proofs, such as this of the Four-Color and Odd Order theorems.

Presentation materials