Lazi

Réalisations présentes et prévues

Réalisation présentes

Une fondation mathématique

C'est le cœur du projet. Elle a des propriétés particulières comme la constructivité et l'extensibilité.
Les preuves de la validité des extensions sont en grande parties déjà faites. Des extensions sont déjà définies.
En savoir plus ...

Un langage informatique

Des 7 règles de déduction Lazi, 5 sont des règles de calcul. Cela permet d'interpréter les formules mathématiques dans un langage très simple (ressemblant, mais en plus simple, au lambda calcul non typé). À partir de ce langage mathématico-informatique on définit un système de types puissant qui est en même temps la notion de structure algébrique en mathématique Lazi.
En savoir plus ...

Un interpréteur du langage informatique

Le langage purement fonctionnel Lazi possède un interpréteur. Grâce à cela on peut par exemple vérifier la validité de preuves Lazi.
Par exemple, ceci est la preuve de a = a :

$L[
    $T[ 'ifOnOne,          $F[if 1b a 0b = a], 		     ∅l ],
    $T[ 'equalArgs,        $F[equal (if 1b a 0b) = equal a], ∅l ],
    $T[ 'equalFuncs,       $F[ (if 1b a 0b = a) = (a = a)],  ∅l ],
    $T[ 'equalityAndTruth, $F[a = a], 			     $D[ x = $F[if 1b a 0b = a] ] ]
]

Réalisation prévue

En mathématiques

  • Finir de définir les extensions de base.
  • Formaliser les preuves déjà faites pour qu'elles puissent être validées.
  • Définir d'autres extensions pour faciliter la production de preuve
  • Définir des extensions pour intégrer les preuves en théorie des ensembles et en théorie des catégories

En informatique théorique

  • Définir un système de vérification des types.

Logiciels

  • Réaliser un compilateur ouvert