LEGO (logiciel)
Un article de Wikipédia, l'encyclopédie libre.
Vous pouvez partager vos connaissances en l’améliorant. (Comment ?).
|
LEGO (1994) est un assistant de preuve interactif, implémenté par Randy Pollack.
Il implémente plusieurs systèmes de types :
- le Logical Framework d'Edimbourg
- le calcul des constructions
- le calcul des constructions généralisé
- la théorie unifiée des types dépendants
Les preuves sont développées dans le style de la déduction naturelle. La synthèse d'argument et le polymorphisme permettent de rendre la formalisation proche des mathématiques informelles.
[modifier] Liens et documents externes
- (en) Le site du projet