Tag : coq

[Fermé]

Découverte de la programmation certifiée avec Coq

Un outil pour écrire des programmes prouvés mathématiquement Par Aabu - Vendredi 01 janvier 2021 à 18h29 01/01/21 à 18h29

10 messages

Dernière réponse
Lundi 29 mars 2021 à 14h29 29/03/21 à 14h29
par Holosmos

[Fermé]

Un zeste de mathématiques assistées par ordinateur

ou comment construire et vérifier des preuves automatiquement Par Aabu - Vendredi 10 avril 2020 à 00h05 10/04/20 à 00h05

8 messages

Dernière réponse
Lundi 18 mai 2020 à 22h18 18/05/20 à 22h18
par anonyme

Problème avec un dependent pattern matching

Comment aider Coq à se souvenir qu’ils font la même taille ? Par lthms - Mardi 03 janvier 2017 à 18h27 03/01/17 à 18h27

1 message

Aucune réponse

Fonctions fortement typés (strongly-specified) en Coq

Discussions autour de cette fonctionnalité de Coq Par lthms - Mercredi 15 juillet 2015 à 23h36 15/07/15 à 23h36

10 messages

Dernière réponse
Vendredi 17 juillet 2015 à 00h09 17/07/15 à 00h09
par anonyme

[Résolu]

Preuves avec propriétés inductives

 Par lthms - Vendredi 26 juin 2015 à 11h42 26/06/15 à 11h42

22 messages

Dernière réponse
Mercredi 15 juillet 2015 à 23h03 15/07/15 à 23h03
par anonyme

VCoq

Un IDE pour Coq 100% dans vim Par QuanticPotato - Jeudi 12 février 2015 à 20h38 12/02/15 à 20h38

1 message

Aucune réponse