Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur GraphSearch.
Cette séance de cours explore la correspondance de Curry-Howard, montrant la relation entre les logiques constructives et les langages de programmation. Il explique comment les preuves en logique correspondent aux preuves en programmation, et comment les types en programmation correspondent aux propositions en logique. La séance de cours se penche sur le concept de simplification de la preuve, également connu sous le nom «élimination de coupe», et mentionne des outils comme Coq, Lean, Agda, Idris, Scala et Haskell.