Courses/LOFO

From LRDE

Titre

Logique formelle

Sigle

LOFO

Enseignant

Adrien Pommellet (Adrien)

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 :

  • Logique propositionnelle et sa sémantique, preuves, systèmes à la Hilbert.
  • Déduction naturelle, logique du premier ordre, normalisation.
  • Lambda calcul, propriétés et applications.
  • Lambda calcul simplement typé, isomorphisme de Curry-Howard.
Documentation
Support
Journaux