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

1 files changed, 158 insertions, 0 deletions

diff --git a/programme-inf110-2025.tex b/programme-inf110-2025.tex
new file mode 100644
index 0000000..855b070
--- /dev/null
+++ b/programme-inf110-2025.tex
@@ -0,0 +1,158 @@
+%% This is a LaTeX document.  Hey, Emacs, -*- latex -*- , get it?
+\documentclass[12pt,a4paper]{article}
+\usepackage[a4paper,hmargin=2cm,vmargin=3cm]{geometry}
+\usepackage[french]{babel}
+\usepackage[utf8]{inputenc}
+\usepackage[T1]{fontenc}
+%\usepackage{ucs}
+\usepackage{times}
+% A tribute to the worthy AMS:
+\usepackage{amsmath}
+\usepackage{amsfonts}
+\usepackage{amssymb}
+\usepackage{amsthm}
+%
+\usepackage{mathrsfs}
+\usepackage{wasysym}
+\usepackage{url}
+%
+\usepackage{graphics}
+\usepackage[usenames,dvipsnames]{xcolor}
+%\usepackage{tikz}
+%\usetikzlibrary{arrows}
+%
+\theoremstyle{definition}
+\newtheorem{comcnt}{Tout}
+\newcommand\thingy{%
+\refstepcounter{comcnt}\smallbreak\noindent\textbf{\thecomcnt.} }
+\renewcommand{\thefootnote}{\fnsymbol{footnote}}
+%
+\DeclareUnicodeCharacter{00A0}{~}
+%
+%
+%
+\begin{document}
+\title{Logique et Fondements de l'Informatique\\Attendus du cours en 2024–2025}
+\author{David A. Madore}
+\maketitle
+
+\centerline{\textbf{INF110}}
+
+{\footnotesize
+\immediate\write18{sh ./vc > vcline.tex}
+\begin{center}
+Git: \input{vcline.tex}
+\end{center}
+\immediate\write18{echo ' (stale)' >> vcline.tex}
+\par}
+
+
+%
+%
+%
+
+\textbf{Sont au programme du cours} les notions suivantes :
+
+\begin{itemize}
+\item \textbf{Calculabilité :} fonctions primitives récursives,
+  fonctions générales récursives, numérotation (notamment la notation
+  $\varphi_e(i)$), théorème s-m-n, astuce de Quine, existence d'une
+  fonction universelle pour les fonctions générales récursives (et
+  inexistence pour les primitives récursives), théorème de la forme
+  normale et possibilité de lancer des calculs en parallèle, théorème
+  de récursion de Kleene ; indécidabilité du problème de l'arrêt,
+  théorème de Rice ; machines de Turing et équivalence avec les
+  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,
+  équivalence du $\lambda$-calcul avec les fonctions générales
+  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 (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
+  preuve, 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 ; 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.
+\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
+  détail pointilleux des notations) ; logique du premier ordre pure,
+  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 ; 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 l'idée
+  de sa démonstration.
+\item \textbf{Coq :} l'utilisation générale de Coq telle que pratiquée
+  en TP, et notamment les principales tactiques de raisonnement (sur
+  les connecteurs logiques, types inductifs, égalités, etc.).  Le nom
+  des tactiques est exigible donc on recommande de préparer un
+  récapitulatif pour l'examen (un tel document est disponible sur la
+  page eCampus du cours).
+\end{itemize}
+
+\bigskip
+
+\textbf{Ne sont explicitement pas exigibles} les notions suivantes :
+
+\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}$.
+\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
+  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 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}
+
+
+%
+%
+%
+\end{document}