Skip to Main content Skip to Navigation
Conference papers

Conteneurs de première classe en Coq

Stéphane Lescuyer 1, 2
2 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : 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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [10 references]  Display  Hide  Download

https://hal.inria.fr/inria-00535659
Contributor : Stéphane Lescuyer <>
Submitted on : Friday, November 12, 2010 - 11:56:37 AM
Last modification on : Wednesday, September 16, 2020 - 5:04:55 PM
Long-term archiving on: : Friday, October 26, 2012 - 3:30:47 PM

File

lescuyer.pdf
Publisher files allowed on an open archive

Identifiers

  • HAL Id : inria-00535659, version 1

Collections

Citation

Stéphane Lescuyer. Conteneurs de première classe en Coq. Journées Françaises des Langages Applicatifs, INRIA, Jan 2010, La Ciotat, France. ⟨inria-00535659⟩

Share

Metrics

Record views

226

Files downloads

266