Courses/LOFO

Titre	Logique formelle
Sigle	LOFO
Enseignant	Adrien Pommellet
Période	S4, Ing1
Public	Tronc-commun
Contrôle	Partiel
Durée	12h
Optionnel	oui
Module	Sciences Générales
Prérequis	Capacité à comprendre et écrire des preuves par récurrence. Capacité à lire des formules mathématiques et à exprimer des propriétés sous forme de formule. Il est souhaitable mais pas obligatoire d'avoir suivi LOGI.
Objectifs	Ce cours présente principalement deux notions théoriques avec des applications concrètes en informatique : Les systèmes de preuves, qui introduisent la notion de vérité comme construction obtenue à partir d'une série de déductions ; des logiciels de preuve comme COQ ou des langages certifiés comme l'Atelier B en dépendent. Le lambda calcul, formalisme de programmation différent des machines de Turing mais tout aussi puissant, que l'on peut typer et qui sert de base à la programmation fonctionnelle. Ces deux notions sont reliées par l'isomorphisme de Curry-Howard. Un programme est donc d'une certaine manière une forme de preuve mathématique.
Plan	Ce cours est découpé en quatre séances : 1) Logique propositionnelle et sa sémantique, preuves, systèmes à la Hilbert. 2) Déduction naturelle, logique du premier ordre, normalisation. 3) Lambda calcul, propriétés et applications. 4) Lambda calcul simplement typé, isomorphisme de Curry-Howard.
Documentation
Support	https://www.lrde.epita.fr/~adrien/notes_logi-lofo_19_20.pdf
Journaux