Skip to Main content Skip to Navigation
Other publications

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 - Formally Verified Programs, Certified Tools and Numerical Computations
LRI - Laboratoire de Recherche en Informatique, Inria Saclay - Ile de France
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 metadata

Cited literature [17 references]  Display  Hide  Download
Contributor : Mário José Parreira Pereira Connect in order to contact the contributor
Submitted on : Wednesday, July 12, 2017 - 12:51:14 PM
Last modification on : Friday, January 21, 2022 - 3:18:41 AM
Long-term archiving on: : Thursday, January 25, 2018 - 4:32:17 AM


Files produced by the author(s)


  • HAL Id : hal-01561094, version 1


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



Les métriques sont temporairement indisponibles