Ce cours met l'accent sur la calculabilité indépendamment des problèmes de complexité. Une donnée est effectivement calculable ou non, indépendamment des conditions en temps ou en mémoire.
Nous passerons en revue les différentes théories de la calculabilité ainsi que le principal résultat qui est la thèse de Church.
Nous verrons en particulier la théorie des combinateurs et le lambda-calcul.
Nous verrons quelques théorèmes d'impossibilité qui en découlent.
Nous montrerons comment la théorie de types résout les paradoxes, la correspondance de Curry-Howard et la réalisabilité.
Mots-clé: Fonctions partielles récursives, Unlimited Register Machine, machine de Turing, théorie des combinateurs, lambda-calcul, typage, logique intuitionniste, isomorphisme de Curry-Howard.
Nous passerons en revue les différentes théories de la calculabilité ainsi que le principal résultat qui est la thèse de Church.
Nous verrons en particulier la théorie des combinateurs et le lambda-calcul.
Nous verrons quelques théorèmes d'impossibilité qui en découlent.
Nous montrerons comment la théorie de types résout les paradoxes, la correspondance de Curry-Howard et la réalisabilité.
Mots-clé: Fonctions partielles récursives, Unlimited Register Machine, machine de Turing, théorie des combinateurs, lambda-calcul, typage, logique intuitionniste, isomorphisme de Curry-Howard.
- Enseignant responsable de l'UE: Jean Leneutre