Nous montrerons comment un langage similaire à ML, peut être transformé de manière très simple et minimaliste en un système de déduction où les preuves sont des programmes.