title: LEGO (logiciel)
text: # LEGO (logiciel)
  
  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
  
  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.
  
  