De nouveaux outils pour calculer avec des inductifs en Coq
En ajoutant au lambda-calcul des structures de données algébriques, des types dépendants et un système de modules, on obtient un langage de programmation avec peu de primitives mais une très grande expressivité. L'assistant de preuve Coq s'appuie sur un tel langage (le CIC) à la sémantique...
| Main Author: | |
|---|---|
| Language: | fra |
| Published: |
Université Paris-Diderot - Paris VII
2014
|
| Subjects: | |
| Online Access: | http://tel.archives-ouvertes.fr/tel-01054723 http://tel.archives-ouvertes.fr/docs/01/05/47/23/PDF/these_boutillier.pdf http://tel.archives-ouvertes.fr/docs/01/05/47/23/ANNEX/soutenace_boutillier.pdf |