Isabelle (logiciel)
Pour les articles homonymes, voir Isabelle.
Cet article est une ébauche concernant l’informatique.
Vous pouvez partager vos connaissances en l’améliorant (comment ?) selon les recommandations des projets correspondants.
Isabelle
| Développé par | Université de technologie de Munich et université de Cambridge |
|---|---|
| Première version | |
| Écrit en | Standard ML et Scala |
| Système d'exploitation | GNU/Linux, Microsoft Windows et macOS |
| Formats lus | Isabelle file format (d) |
| Formats écrits | Isabelle file format (d) |
| Type |
Assistant de preuve Logiciel à sources consultables (en) |
| Licence | Licence BSD |
| Site web | isabelle.in.tum.de |
Le logiciel Isabelle est un assistant de preuve, c'est-à-dire un démonstrateur interactif de théorèmes. C'est le successeur de HOL (en).
C’est un logiciel libre publié sous licence BSD.
Cette section est vide, insuffisamment détaillée ou incomplète. Votre aide est la bienvenue ! Comment faire ?
Liens externes
[modifier | modifier le code]- (en) Site web officiel Isabelle
- (en) The Archive of Formal Proofs
- (en) IsarMathLib
