Machines de Turing non déterministes : équivalence avec les machines de Turing du point de vue de la calculabilité. Définition de la classe NP comme la classe des problèmes résolubles en temps polynomial par une machine de Turing non déterministe, équivalence avec l’acceptation par certificat.
Définitions et caractérisations des ensembles récursifs, récursivement énumérables.
Fonctions récursives : définition, équivalence avec les machines de Turing.
Lambda-calcul pur comme modèle de calcul : définition, propriétés (dont confluence), stratégies. Équivalence avec les machines de Turing et les fonctions récursives.
Thèse de Church-Turing.
Logique
Logique du premier ordre (aspects syntaxiques) : langages, termes, formules, variables libres et variables liées, substitutions, capture de variables.
Logique du premier ordre (aspects sémantiques) : interprétation d’une formule dans un modèle, validité, satisfiabilité, théories cohérentes, théories complètes, théories décidables, indécidables. Exemples de théories : égalité, arithmétique de Peano.
Bases de données : calcul relationnel et théorème de Codd.
Fondements de la programmation
Preuve de programmes : correction, terminaison, logique de Hoare, induction structurelle.
Sémantique des langages de programmation : sémantiques opérationnelles.
Application à un langage impératif restreint (IMP).
Systèmes de types : types simples. Application à un langage fonctionnel simple
(mini-ML sans polymorphisme), sûreté du typage.