Appears in collection : Workshop Schlumberger : Types dépendants et Formalisation des mathématiques

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.