Retourner au contenu associé (dépêche : Sortie de Coq 8.5 bêta, un assistant de preuve formelle)
Posté par patrick_g (site web personnel) le 28 janvier 2015 à 14:37. En réponse à la dépêche Sortie de Coq 8.5 bêta, un assistant de preuve formelle. Évalué à 10. Dernière modification le 28 janvier 2015 à 15:53.
Comme les autres je ne peux que dire merci pour cette belle dépêche. Pour les plus courageux il y avait eu un numéro spécial des Notices de l'American Mathematical Society qui était consacré aux preuves formelles et à Coq/HOL/Isabelle :
http://www.ams.org/notices/200811/index.html
Je recommande particulièrement l'article "Formal Proof - Getting Started".
AltStyle によって変換されたページ (->オリジナル) / アドレス: モード: デフォルト 音声ブラウザ ルビ付き 配色反転 文字拡大 モバイル
# Notices of AMS
Posté par patrick_g (site web personnel) . En réponse à la dépêche Sortie de Coq 8.5 bêta, un assistant de preuve formelle. Évalué à 10. Dernière modification le 28 janvier 2015 à 15:53.
Comme les autres je ne peux que dire merci pour cette belle dépêche.
Pour les plus courageux il y avait eu un numéro spécial des Notices de l'American Mathematical Society qui était consacré aux preuves formelles et à Coq/HOL/Isabelle :
http://www.ams.org/notices/200811/index.html
Je recommande particulièrement l'article "Formal Proof - Getting Started".