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
Inria Saclay - Ile de France, LRI - Laboratoire de Recherche en Informatique
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 : Thursday, October 3, 2019 - 2:04:03 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

522

Files downloads

301