%% 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 2025–2026}
\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, 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}$ 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
  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 ; 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
  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) ; 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
  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 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é, 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
  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}
