From 5a2c2febd2c963e58142edaf809f0a4cac806561 Mon Sep 17 00:00:00 2001 From: "David A. Madore" Date: Thu, 30 Oct 2025 13:59:51 +0100 Subject: Note Coq→Rocq name change. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- transp-inf110-02-typage.tex | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'transp-inf110-02-typage.tex') 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} -- cgit v1.2.3