diff options
Diffstat (limited to 'transp-inf110-02-typage.tex')
| -rw-r--r-- | transp-inf110-02-typage.tex | 6 |
1 files changed, 3 insertions, 3 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} |