LEGO (logiciel)

Un article de Wikipédia, l'encyclopédie libre.
Ceci est la version actuelle de cette page, en date du 1 octobre 2016 à 01:14 et modifiée en dernier par Mule hollandaise (discuter | contributions). L'URL présente est un lien permanent vers cette version.
(diff) ← Version précédente | Voir la version actuelle (diff) | Version suivante → (diff)

Cet article est une ébauche concernant un logiciel et les mathématiques.

Vous pouvez partager vos connaissances en l’améliorant (comment ?) selon les recommandations des projets correspondants.

Page d’aide sur l’homonymie

Pour les articles homonymes, voir Lego (homonymie).

LEGO, est un assistant de preuve interactif, créé par Randy Pollack en 1994

Il possède 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
[Quoi ?]

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[Quoi ?].

Liens externes[modifier | modifier le code]

Ce document provient de « https://fr.wikipedia.org/w/index.php?title=LEGO_(logiciel)&oldid=130195004 ».