Syllabus for 2025–2026 (and commit past years' versions).

1 files changed, 19 insertions, 18 deletions

diff --git a/programme-inf110.tex b/programme-inf110.tex
index 855b070..bc2b72d 100644
--- a/programme-inf110.tex
+++ b/programme-inf110.tex
@@ -32,7 +32,7 @@
 %
 %
 \begin{document}
-\title{Logique et Fondements de l'Informatique\\Attendus du cours en 2024–2025}
+\title{Logique et Fondements de l'Informatique\\Attendus du cours en 2025–2026}
 \author{David A. Madore}
 \maketitle
 
@@ -65,10 +65,12 @@ Git: \input{vcline.tex}
   fonctions générales récursives ; parties décidables et
   semi-décidables, équivalence entre semi-décidable et « image d'une
   fonction calculable » ; la notion de réduction many-to-one et de
-  Turing ; le $\lambda$-calcul non typé, $\beta$-réduction, théorème
-  de Church-Rosser, redex extérieur gauche, entiers de Church,
+  Turing, la définition des degrés many-to-one et de Turing ; le
+  $\lambda$-calcul non typé, $\beta$-réduction, théorème de
+  Church-Rosser, redex extérieur gauche, entiers de Church,
   équivalence du $\lambda$-calcul avec les fonctions générales
-  récursives, combinateur $\mathsf{Y}$.
+  récursives, combinateur $\mathsf{Y}$ et son utilisation pour les
+  appels récursifs.
 \item \textbf{Typage :} $\lambda$-calcul simplement typé, et sa
   version enrichie par les types produits, sommes, $1$ et $0$ ;
   terminaison des programmes écrits dans ce dernier (normalisation
@@ -83,12 +85,11 @@ Git: \input{vcline.tex}
   classique ; propriété de la disjonction et décidabilité du calcul
   propositionnel intuitionniste (idée).
 \item \textbf{Sémantiques du calcul propositionnel intuitionniste :}
-  sémantique des ouverts, sa correction et sa complétude ; définition
-  de la sémantique de la rélisabilité propositionnelle, et sa
-  correction ; savoir utiliser \emph{au moins une} des sémantiques
-  vues en cours (ouverts, réalisabilité propositionnelle,
-  éventuellement Kripke ou les problèmes finis) pour montrer qu'une
-  formule propositionnelle n'est pas démontrable.
+  sémantique des ouverts, sa correction et sa complétude ; sémantique
+  de Kripke, sa correction et sa complétude ; définition de la
+  sémantique de la rélisabilité propositionnelle, et sa correction ;
+  utilisation de la correction des sémantiques vues en cours pour
+  montrer qu'une formule propositionnelle n'est pas démontrable.
 \item \textbf{Quantificateurs :} règles \emph{générales}
   d'introduction et d'élimination du $\forall$ et $\exists$, et
   $\lambda$-termes de preuve correspondants (sans entrer dans le
@@ -117,10 +118,10 @@ Git: \input{vcline.tex}
 \begin{itemize}
 \item Les détails de la fonction d'Ackermann ; les détails de la
   notion d'arbre de calcul (autre que l'énoncé du théorème de la forme
-  normale) ; la notion de degré many-to-one ou de Turing ; les notions
-  de $\beta$-réduction autres qu'extérieur gauche, les subtilités de
-  l'ordre d'évaluation, le combinateur $\mathsf{Z}$ ou sa différence
-  avec $\mathsf{Y}$.
+  normale) ; rien d'autre sur les réductions degrés many-to-one et de
+  Turing que leur définition ; les notions de $\beta$-réduction autres
+  qu'extérieur gauche, les subtilités de l'ordre d'évaluation, le
+  combinateur $\mathsf{Z}$ ou sa différence avec $\mathsf{Y}$.
 \item Les détails du typage de quelque langage de programmation que ce
   soit (autres que les variantes du $\lambda$-calcul simplement typé
   vus en cours, et les parties de Coq vues en TP), notamment rien de
@@ -136,12 +137,12 @@ Git: \input{vcline.tex}
   continuation-passing-style ou de son typage.  Le
   $\lambda\mu$-calcul.
 \item Les subtilités de la réalisabilité propositionnelle (p.ex., la
-  réalisabilité de la formule de Tseitin).  La sémantique de Kripke et
-  celle des problèmes finis ne sont pas exigibles (mais pourront être
-  utilisées si on le souhaite).
+  réalisabilité de la formule de Tseitin).  La sémantique des
+  problèmes finis n'est pas exigible (mais pourra être utilisée si on
+  le souhaite).
 \item Le $\lambda$-cube de Barendregt, les subtilités de la différence
   entre $\exists$ et types sommes, la notion de
-  prédicativité/imprédicativité.
+  prédicativité/imprédicativité, le système $F$.
 \item Les subtilités des différences et rapports entre l'arithmétique
   de Heyting et celle de Peano (sauf s'il s'agit, par exemple, de
   vérifier si une démonstration donnée utilise un raisonnement par