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 postpone the others. On the user side, a modern interface based on the PIDE middleware aggregates and presents in a consistent way the output of the prover. Finally postponed tasks are processed exploiting modern, parallel, hardware to offer better scalability.
Cite
CITATION STYLE
Barras, B., Tankink, C., & Tassi, E. (2015). Asynchronous processing of Coq documents: From the kernel up to the user interface. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9236, pp. 51–66). Springer Verlag. https://doi.org/10.1007/978-3-319-22102-1_4
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
