21 citations · 54 across the 7 of their papers we have counts for
Showing 2013Show all
2 papers · 1 filter
cs.LO2013
The Rooster and the Syntactic Bracket
Hugo Herbelin, Arnaud Spiwack
We propose an extension of pure type systems with an algebraic presentation of inductive and co-inductive type families with proper indices. This type theory supports coercions tow…
cs.LO2013★ 1 cited
Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems
Bruno Barras, Lourdes del Carmen González Huesca, Hugo Herbelin +4
This is an overview of the Paral-ITP project, which intents to make the proof assistants Isabelle and Coq fit for the multicore era.