From cd521ecc61adceeda61ac67f589be3c0c3964b8c Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Tue, 21 Jan 2025 11:22:17 +0100
Subject: Update syllabus.

---
 programme-inf110.tex | 90 ++++++++++++++++++++++++----------------------------
 1 file changed, 42 insertions(+), 48 deletions(-)

(limited to 'programme-inf110.tex')

diff --git a/programme-inf110.tex b/programme-inf110.tex
index ed105ae..c6217c7 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 2023–2024}
+\title{Logique et Fondements de l'Informatique\\Attendus du cours en 2024–2025}
 \author{David A. Madore}
 \maketitle
 
@@ -71,27 +71,24 @@ Git: \input{vcline.tex}
   récursives, combinateur $\mathsf{Y}$.
 \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 (sans détails) ;
-  correspondance de Curry-Howard entre $\lambda$-calcul simplement
-  typé enrichi et calcul propositionnel intuitionniste ; algorithme de
-  Hindley-Milner (basique).
+  terminaison des programmes écrits dans ce dernier (normalisation
+  forte ; sans preuve ni détails) ; correspondance de Curry-Howard
+  entre $\lambda$-calcul simplement typé enrichi et calcul
+  propositionnel intuitionniste.
 \item \textbf{Calcul propositionnel :} règles de logique en déduction
   naturelle, et au moins une présentation des preuves (arbre de
   séquents, ou drapeau) ; écriture et vérification des
   $\lambda$-termes de preuve (sans entrer dans le détail pointilleux
   des notations) ; différence entre logique intuitionniste et logique
-  classique ; notion de calcul des séquents et de preuve sans coupure
-  (sans détails) ; notions des axiomes de Hilbert / combinateurs
-  $\mathsf{S},\mathsf{K},\mathsf{I}$ (sans détails).
-\item \textbf{Continuations et call/cc :} la notion générale de
-  continuation, l'idée générale de la fonction call/cc et son rapport
-  avec la loi de Peirce, l'idée générale du continuation-passing-style
-  (sans détails).
+  classique ; propriété de la disjonction et décidabilité du calcul
+  propositionnel intuitionniste (idée).
 \item \textbf{Sémantiques du calcul propositionnel intuitionniste :}
-  \emph{au moins une} des quatre sémantiques vues en cours (Kripke,
-  ouverts, réalisabilité propositionnelle, problèmes finis), sa
-  correction, et comment on s'en sert pour montrer qu'une formule
-  propositionnelle n'est pas démontrable.
+  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.
 \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
@@ -99,12 +96,14 @@ Git: \input{vcline.tex}
   logique du premier ordre avec égalité.
 \item \textbf{Arithmétique du premier ordre :} les axiomes de Peano ;
   l'idée générale que Curry-Howard sur l'arithmétique de Heyting
-  permet d'extraire des algorithmes des preuves ; la possibilité de
-  formaliser $\varphi_e(i){\downarrow}$ en arithmétique de
+  permet d'extraire des algorithmes des preuves ; le fait qu'il est
+  possible formaliser $\varphi_e(i){\downarrow}$ en arithmétique de
   Heyting/Peano ; le fait que vérifier si une preuve est valable est
   décidable, mais que savoir si un énoncé est un théorème est
-  seulement semi-décidable ; l'énoncé du théorème de Gödel et au moins
-  une certaine idée de la preuve par machines de Turing.
+  seulement semi-décidable ; l'énoncé du théorème de Gödel et l'idée
+  de sa démonstration.
+\item \textbf{Coq :} l'utilisation générale de Coq telle que pratiquée
+  en TP.
 \end{itemize}
 
 \bigskip
@@ -120,37 +119,32 @@ Git: \input{vcline.tex}
   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, Hindley Milner, et les parties de Coq vues en TP),
-  notamment rien de ce qui concerne Scheme, Haskell ou quelque autre
-  langage mentionné en passant dans le cours ; le sous-typage, le
-  polymorphisme ad hoc, les types dépendants, ou les autres
-  fonctionnalités de certains systèmes de typages mentionnés en
-  passant dans le cours.  Les subtilités de l'algorithme de
-  Hindley-Milner (problème du polymorphisme du \texttt{let},
-  restriction de valeur).
-\item Les subtilités des règles structurales en calcul des séquents.
-  Le fonctionnement de l'élimination des coupures ou sa preuve.  Le
-  $\overline{\lambda}$-calcul (juste mentionné en cours).  Le détail
-  de l'équivalence entre déduction naturelle et calcul des séquents.
-  Le détail de l'élimination des $\lambda$ grâce aux combinateurs
-  $\mathsf{S},\mathsf{K},\mathsf{I}$.
-\item Le fonctionnement détaillé de la fonction call/cc.  Les détails
-  du continuation-passing-style (conversion systématique) ou de son
-  typage.  Le $\lambda\mu$-calcul (juste mentionné en cours).
-\item La complétude de telle ou telle sémantique du calcul
-  propositionnel intuitionniste.  Les subtilités de la réalisabilité
-  propositionnelle (p.ex., la réalisabilité de la formule de Tseitin).
-  La sémantique des problèmes finis.
+  vus en cours, et les parties de Coq vues en TP), notamment rien de
+  ce qui concerne Scheme, Haskell ou quelque autre langage mentionné
+  en passant dans le cours ; le sous-typage, le polymorphisme ad hoc,
+  les types dépendants, ou les autres fonctionnalités de certains
+  systèmes de typages mentionnés en passant dans le cours.
+  L'algorithme de Hindley-Milner.
+\item Le calcul des séquents, le fonctionnement de l'élimination des
+  coupures ou sa preuve.  Le $\overline{\lambda}$-calcul.  Les axiomes
+  de Hilbert, et les combinateurs $\mathsf{S},\mathsf{K},\mathsf{I}$.
+\item La notion de continuation.  La fonction call/cc.  Le
+  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).
 \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é.
-\item Les détails de Curry-Howard pour quoi que ce soit d'autre que le
-  calcul propositionnel intuitionniste.
-\item Les subtilités des différences et rapports entre Heyting et
-  Peano (sauf s'il s'agit, par exemple, de vérifier si une
-  démonstration donnée utilise un raisonnement par l'absurde).
-\item Les détails de la démonstration du théorème de Gödel, les
-  systèmes précis auxquels il s'applique.
+\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
+  l'absurde).
+\item Les détails de la démonstration du théorème de Gödel, la
+  formalisation des systèmes précis auxquels il s'applique.
+\item Les détails de la syntaxe de Coq.
 \end{itemize}
 
 
-- 
cgit v1.2.3

