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.
Type de document :
Autre publication
ML Family Workshop 2017. 2017
Liste complète des métadonnées

Littérature citée [18 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01561094
Contributeur : Mário José Parreira Pereira <>
Soumis le : mercredi 12 juillet 2017 - 12:51:14
Dernière modification le : vendredi 14 juillet 2017 - 01:09:24

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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. ML Family Workshop 2017. 2017. 〈hal-01561094〉

Partager

Métriques

Consultations de
la notice

168

Téléchargements du document

80