Name
Abstract | ||
|---|---|---|
This paper presents the formal verification with the Coq proof assistant of several applicative data structures implementing finite sets. These implementations are parameterized by an ordered type for the elements, using functors from the ML module system. The verification follows closely this scheme, using the newly Coq module system. One of the verified implementation is the actual code for sets and maps from the Objective Caml standard library. The formalization refines the informal specifications of these libraries into formal ones. The process of verification exhibited two small errors in the balancing scheme, which have been fixed and then verified. Beyond these verification results, this article illustrates the use and benefits of modules and functors in a logical framework. |
Year | DOI | Venue |
|---|---|---|
2004 | 10.1007/978-3-540-24725-8_26 | Lecture Notes in Computer Science |
Keywords | Field | DocType |
logical framework,formal verification,data structure | Data structure,Discrete mathematics,Parameterized complexity,Programming language,Computer science,Formal specification,Theoretical computer science,Functor,Mathematical proof,Logical framework,Formal verification,Proof assistant | Conference |
Volume | ISSN | Citations |
2986 | 0302-9743 | 15 |
PageRank | References | Authors |
1.07 | 7 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jean-Christophe Filliatre | 1 | 64 | 4.65 |
| Pierre Letouzey | 2 | 143 | 8.84 |