Formalization of Mathematics in Type Theory. Generic tools of Modelisation and Demonstration. Application to Category Theory

Autor: Saibi, Amokrane

Publikováno v: Autre [cs.OH]. Université Pierre et Marie Curie-Paris VI, 1999. Français. ⟨NNT : ⟩
Autre [cs.OH]. Université Pierre et Marie Curie-Paris VI, 1999. Français

Formalization of Mathematics in Type Theory. Generic tools of Modelisation and Demonstration. Application to Category Theory; Outils Génériques de Modélisation et de Démonstration pour la Formalisation des Mathématiques en Théorie des Types. Ap

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::376e960856aa962bd14f814b98277e66
https://theses.hal.science/tel-00523810

Axiomatisation d'un Lambda-Calcul avec Substitutions Explicites dans Coq

Autor: Saibi, Amokrane

Publikováno v: [Rapport de recherche] RR-2345, INRIA. 1994

Projet COQ; Nous présentons l'axiomatisation de la théorie du $\Lenv$-calcul dans le système Coq. Le principal résultat axiomatisé est la confluence de ce calcul. Par ailleurs, nous proposons un codage uniforme des systèmes de réécriture à u

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::d68140413cdc67e7b6869da22a6d7db6
https://inria.hal.science/inria-00074332