Je mets ici les cours que j'ai écrits ou que je suis en train d'écrire. La plupart concernent l'informatique théorique ou les mathématiques relativement élémentaires.
Pour l'instant il y a 3 cours :
- un cours de logique compilant ce que j'ai appris dans ce domaine. Il reste à y faire :
- les problèmes d'unification pour l'algorithme de typage
- un peu de sémantique dénotationnelle du lambda-calcul non typé avec les algèbres combinatoires et l'espace Dinf
- l'interprétation BHK et l'isomorphisme de Curry-Howard en lui-même, la gestion des coupures
- le système F
- les types dépendants et la gestion des quantificateurs (avec aussi la logique du premier ordre)
- La partie sur la théorie des catégories
- un cours reprenant le programme de lycée mais en construisant et démontrant les objets et résultats avec un point de vue plus proche du supérieure. Il reste à y faire :
- l'unification du style le long des parties pour avoir quelque chose de plus homogène
- l'ajout d'exercices variés et plus ou moins proches du cours
- la relecture pour enlever les typos
- peut-être ajouter des corrections aux exercices
- un cours d'introduction à la sémantique dénotationnelle. Le projet était plutôt de construire une sémantique jouet d'une version faible de OCaml, et je n'ai pas particulièrement l'ambition d'améliorer ce cours.