Théorie des types et isomorphisme de Curry-Howard : la profonde harmonie entre propositions = types et preuves = programmes
