Conteneurs de première classe en Coq
Résumé
We present a Coq library for finite sets and maps which brings the same functionalities as the existing FSets/FMaps library, but uses type-classes instead of modules in order to ensure the genericity of the proposed data structures. This architecture facilitates the use of these data structures and more generally the implementation of complex algorithms in Coq.
Nous présentons une bibliothèque Coq d'ensembles et de dictionnaires finis qui reproduit les fonctionnalités disponibles dans la bibliothèque existante FSets/FMaps mais où la généricité des structures est obtenue via des classes de types et non des modules. Cette architecture permet un usage simplifié de ces structures et facilite la programmation d'algorithmes complexes en Coq.
Domaines
Logique en informatique [cs.LO]
Origine : Fichiers éditeurs autorisés sur une archive ouverte
Loading...