%% This is a LaTeX document.  Hey, Emacs, -*- latex -*- , get it?
\documentclass[12pt,a4paper]{article}
\usepackage[a4paper,hmargin=2cm,vmargin=3cm]{geometry}
\usepackage[shorthands=off,french]{babel}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage{newtxtext}
% 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}
\usepackage{hyperref}
%
\theoremstyle{definition}
\newtheorem{comcnt}{Tout}
\newcommand\thingy{%
\refstepcounter{comcnt}\smallbreak\noindent\textbf{\thecomcnt.} }
\renewcommand{\thefootnote}{\fnsymbol{footnote}}
%
\DeclareUnicodeCharacter{00A0}{~}
\DeclareUnicodeCharacter{2026}{...}
%
%
%
\begin{document}
\title{Logique et Fondements de l'Informatique\\Bibliographie et conseils de lecture}
\author{David A. Madore}
\maketitle

\centerline{\textbf{CSC-3TC34-TP / INF110}}

{\footnotesize
\immediate\write18{sh ./vc > vcline.tex}
\begin{center}
Git: \input{vcline.tex}
\end{center}
\immediate\write18{echo ' (stale)' >> vcline.tex}
\par}


%
%
%

\setlength{\parskip}{6pt plus 6pt}

Ce document rassemble quelques conseils de lecture pour
\emph{prolonger} ou bien \emph{compléter} le cours de « Logique et
Fondements de l'Informatique », ou simplement en rapport avec des
thématiques évoquées dans ce cours.

\begin{itemize}
\item\setlength{\parskip}{6pt plus 6pt}Commençons par un livre de
  vulgarisation, qui est aussi un grand classique (et une référence de
  toute une génération de geeks): \textit{Gödel, Escher, Bach} de
  Douglas Hofstadter (1979).

C'est un livre très difficile à classer, ou même à décrire, puisqu'il
intercale des chapitres sérieux avec des dialogues humoristiques, et
qu'il parle à la fois de sciences et d'art (ça va des maths à la
biologie en passant par la physique, la linguistique, la philosophie
zen, la linguistique…  et bien sûr les dessins d'Escher et la musique
de Bach, ainsi que des réflexions sur l'intelligence artificielle qui
restent étonnamment pertinentes pas loin de 50 ans après).  Le thème
général est celui de la récursion et de l'auto-référence (et en
particulier, de variations sur le théorème de Gödel et l'astuce de
Quine).  On trouve aussi dedans une formalisation précise de
l'arithmétique du premier ordre (mais présentée à un niveau grand
public) ainsi qu'une description d'un langage de programmation
(« BlooP ») qui calcule précisément les fonctions primitives
récursives.

En tout cas, je recommande très vivement ce livre (à la
lecture duquel je dois beaucoup d'être moi-même devenu mathématicien)
à tous ceux qui trouvent intéressants les thèmes abordés par ce cours.

L'original est en anglais, mais il y a une excellente traduction
française, à laquelle l'auteur lui-même a contribué.

\item Sur la \textbf{calculabilité}, il existe de nombreux ouvrages,
  parmi lesquels on peut par exemple recommander :
\begin{itemize}
\item\textit{Computability Theory} de Barry Cooper (2003) : assez
  court et pas trop indigeste
\item\textit{Calculabilité} de Benoît Monin \& Ludovic Patey (2022) :
  beaucoup plus complet, mais très bien présenté
\item\textit{Turing Computability: Theory and Applications} de Robert
  I. Soare (2016) : concis et complet
\item\textit{Computability Theory: An Introduction to Recursion
  Theory} de Herbert B. Enderton (2011) : beaucoup plus élémentaire et
  moins complet que les précédents
\end{itemize}

\item\setlength{\parskip}{6pt plus 6pt}Sur le \textbf{typage}, le
  livre \textit{Types and Programming Languages} de Benjamin Pierce
  (2002) aborde les aspects à la fois théoriques et pratiques du
  typage dans différents langages de programmation de manière bien
  plus complète que ce que j'ai pu faire en cours.

Beaucoup plus costaud : {\textit{Proofs and Types}} de Jean-Yves
Girard (disponible à l'adresse
\url{http://www.paultaylor.eu/stable/prot.pdf} ; il s'agit de la
traduction anglaise d'un original français, mais je crois que
l'original est devenu introuvable).  Contient des définitions précises
de divers systèmes logiques et de typage, la preuve de leur
normalisation, et les explications mathématiquement précises sur la
correspondance de Curry-Howard.

\item\setlength{\parskip}{6pt plus 6pt}Sur le \textbf{théorème de
  Gödel} : \textit{Gödel's Theorem (An Incomplete Guide to its Use and
  Abuse)} de Torkel Franzén (2005) est un ouvrage de
  semi-vulgarisation très bien écrit, et il prend notamment le temps
  d'expliquer plein de malentendus sur l'usage fait de ce théorème
  (notamment par des non-mathématiciens).

Je peux aussi recommander \textit{An Introduction to Gödel's Theorems}
de Peter Smith (Cambridge University Press, 2013), qui est moins de la
vulgarisation et plus précis et complet, et qui est également très
bien écrit, mais il est difficile à trouver.

\item\setlength{\parskip}{6pt plus 6pt}Sur la \textbf{programmation
  fonctionnelle} : si ce style de programmation vous intéresse, je
  vous recommande fortement d'apprendre au moins un des langages de
  programmation Scheme (non typé, proche du $\lambda$-calcul) et/ou
  Haskell (fortement typé, mais diffère du OCaml en ce qu'il est
  « paresseux » et « purement fonctionnel », c'est-à-dire sans effets
  de bord, et c'est très instructif de comprendre ce que cela permet).

\item\setlength{\parskip}{6pt plus 6pt}Concernant la programmation
  fonctionnelle \textbf{non typée}, le livre \textit{Structure and
    Interpretation of Computer Programs} d'Abelson et Sussman (1996 ;
  aussi appelé le « Wizard Book », aussi bien en référence à
  l'illustration de couverture que la compétence qu'il vous fera
  acquérir) est un grand classique, qui a servi pendant des années de
  support de cours au MIT.  Il est épuisé au format papier, mais il
  est librement disponible en ligne à l'adresse
  \url{https://web.mit.edu/6.001/6.037/sicp.pdf} sur le site du MIT.
  Il est basé sur le Scheme (mais ne présuppose pas la connaissance du
  Scheme), mais il ne s'agit pas non plus d'un cours de Scheme : il
  s'agit d'un cours de programmation fonctionnelle non typée et des
  concepts fondamentaux qui vont avec.  (Il y a aussi une “édition
  JavaScript” du livre, plus récente, si vous préférez ce langage ;
  mais je ne sais pas ce qu'elle vaut.)

Notamment, ce livre explique comment écrire un interpréteur Scheme en
Scheme (et ensuite comment le modifier), autrement dit, un programme
universel, et ce que ça nous apprend sur la programmation et la
sémantique des languages de programmation.  (L'exposé \textit{The Most
  Beautiful Program Ever Written} de William Byrd, disponible sur
YouTube à l'adresse \url{https://www.youtube.com/watch?v=OyfBQmvr2Hc},
peut également être intéressant comme une sorte de version très
abrégée de ce point.)

Le livre de Christian Queinnec \textit{Lisp in Small Pieces} (2007 ;
traduction d'un original français \textit{Les langages Lisp} devenu
introuvable) est également très instructif.

\item\setlength{\parskip}{6pt plus 6pt}Concernant la programmation
  fonctionnelle \textbf{typée}, outre le OCaml, le Haskell est un
  langage très intéressant (y compris mathématiquement).  À son sujet,
  le livre de Christopher Allen et Julie Moronuki \textit{Haskell
    Programming from first principles} me semble bien (il n'existe pas
  au format papier, mais le PDF est achetable en ligne à l'adresse
  \url{https://haskellbook.com/}).
\end{itemize}

\bigskip

J'aurai certainement des ajouts à faire à cette liste ultérieurement.


%
%
%
\end{document}