Asynchronous processing of Coq documents: from the kernel up to the user interface

Abstract : The work described in this paper improves the reactivity of the Coq system by completely redesigning the way it processes a formal document. By subdividing such work into independent tasks the system can give precedence to the ones of immediate interest for the user and postpones the others. On the user side, a modern interface based on the PIDE middleware aggregates and present in a consistent way the output of the prover. Finally postponed tasks are processed exploiting modern, parallel, hardware to offer better scalability.
Type de document :
Communication dans un congrès
Proceedings of ITP, Aug 2015, Nanjing, China
Liste complète des métadonnées


https://hal.inria.fr/hal-01135919
Contributeur : Enrico Tassi <>
Soumis le : mercredi 17 juin 2015 - 09:52:08
Dernière modification le : samedi 18 février 2017 - 01:14:43

Fichiers

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

Licence


Copyright (Tous droits réservés)

Identifiants

  • HAL Id : hal-01135919, version 1
  • ARXIV : 1506.05605

Collections

Citation

Bruno Barras, Carst Tankink, Enrico Tassi. Asynchronous processing of Coq documents: from the kernel up to the user interface. Proceedings of ITP, Aug 2015, Nanjing, China. <hal-01135919>

Partager

Métriques

Consultations de
la notice

205

Téléchargements du document

148