diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 6 | ||||
| -rw-r--r-- | transp-inf110-03-quantif.tex | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index 9082576..71547c7 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -562,7 +562,7 @@ fonctions p.r. \bigskip -Exemple de tel langage : Coq. +Exemple de tel langage : Coq (maintenant appelé Rocq). \end{frame} % @@ -716,7 +716,7 @@ tacite qu'on peut construire un tel $A$. \itempoint Langages spécialisés pour servir à la fois à l'écriture de programmes informatiques et de preuves mathématiques ; ils peuvent être soit sous forme de systèmes abstraits, soit sous forme -d'implémentation informatique (« assistants de preuve » : Coq, Agda, +d'implémentation informatique (« assistants de preuve » : Coq/Rocq, Agda, Lean…). \bigskip @@ -769,7 +769,7 @@ n'a aucune des trois, CoC a les trois) : \medskip {\footnotesize On peut ensuite encore ajouter des fonctionnalités : - par exemple, Coq est basé sur le « calcul des constructions + par exemple, Coq/Rocq est basé sur le « calcul des constructions inductives » qui ajoute au calcul des constructions des mécanismes systématiques pour former des types (positivement !) récursifs.\par} diff --git a/transp-inf110-03-quantif.tex b/transp-inf110-03-quantif.tex index 07c5d43..61063b9 100644 --- a/transp-inf110-03-quantif.tex +++ b/transp-inf110-03-quantif.tex @@ -542,7 +542,7 @@ monde des démonstrations, plus simples, ou différentes. \medskip -\itempoint En Coq, les deux mondes sont \alert{séparés mais +\itempoint En Coq/Rocq, les deux mondes sont \alert{séparés mais parallèles} : $\mathit{Prop}$ pour le type des propositions et $\mathit{Type}$ pour le type des types d'individus. |