17 citations · 17 across the 2 of their papers we have counts for
Showing cs.LOShow all
2 papers · 1 filter
cs.LO2021
Implementation of Two Layers Type Theory in Dedukti and Application to Cubical Type Theory
Bruno Barras, Valentin Maestracci
In this paper, we make a substantial step towards an encoding of Cubical Type Theory (CTT) in the Dedukti logical framework. Type-checking CTT expressions features a decision proce…
cs.LO2015★ 17 cited
Asynchronous processing of Coq documents: from the kernel up to the user interface
Bruno Barras, Carst Tankink, Enrico Tassi
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 independe…