VOCAL – A Verified OCAml Library

Arthur Charguéraud 1, 2 Jean-Christophe Filliâtre 3 Mário Pereira 3 François Pottier 2
1 CAMUS - Compilation pour les Architectures MUlti-coeurS
Inria Nancy - Grand Est, ICube - Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie
3 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Abstract : ▼Abstract Libraries are the basic building blocks of any realistic programming project. It is thus of utmost interest for a programmer to build her software on top of bug-free libraries. We present the ongoing VOCAL project, which aims at building a mechanically verified library of general-purpose data structures and algorithms, written in the OCaml language.
Document type :
Other publications
Complete list of metadatas

Cited literature [17 references]  Display  Hide  Download

https://hal.inria.fr/hal-01561094
Contributor : Mário José Parreira Pereira <>
Submitted on : Wednesday, July 12, 2017 - 12:51:14 PM
Last modification on : Monday, November 26, 2018 - 1:28:02 PM
Long-term archiving on : Thursday, January 25, 2018 - 4:32:17 AM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01561094, version 1

Citation

Arthur Charguéraud, Jean-Christophe Filliâtre, Mário Pereira, François Pottier. VOCAL – A Verified OCAml Library. 2017. ⟨hal-01561094⟩

Share

Metrics

Record views

505

Files downloads

290