Propositions en tant que types: Logique et correspondance de programmation

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.