diff options
| author | David A. Madore <david+git@madore.org> | 2025-10-30 13:59:51 +0100 |
|---|---|---|
| committer | David A. Madore <david+git@madore.org> | 2025-10-30 13:59:51 +0100 |
| commit | 5a2c2febd2c963e58142edaf809f0a4cac806561 (patch) | |
| tree | 189a1eb41966ee8236e262d5847d73cb382e9d1c /transp-inf110-02-typage.tex | |
| parent | 9cea2929c6f53a485994553ef8cef720c8d763be (diff) | |
| download | inf110-lfi-5a2c2febd2c963e58142edaf809f0a4cac806561.tar.gz inf110-lfi-5a2c2febd2c963e58142edaf809f0a4cac806561.tar.bz2 inf110-lfi-5a2c2febd2c963e58142edaf809f0a4cac806561.zip | |
Note Coq→Rocq name change.
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} |