Skip to Main content Skip to Navigation
New interface
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 metadata

Cited literature [10 references]  Display  Hide  Download
Contributor : Stéphane Lescuyer Connect in order to contact the contributor
Submitted on : Friday, November 12, 2010 - 11:56:37 AM
Last modification on : Sunday, June 26, 2022 - 11:52:35 AM
Long-term archiving on: : Friday, October 26, 2012 - 3:30:47 PM


Publisher files allowed on an open archive


  • HAL Id : inria-00535659, version 1



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⟩



Record views


Files downloads