21 citations · 54 across the 7 of their papers we have counts for
7 papers · 1 filter
A parametricity-based formalization of semi-simplicial and semi-cubical sets
Hugo Herbelin, Ramkumar Ramachandra
Semi-simplicial and semi-cubical sets are commonly defined as presheaves over respectively, the semi-simplex or semi-cube category. Homotopy Type Theory then popularized an alterna…
On the logical structure of choice and bar induction principles
Nuria Brede, Hugo Herbelin
We develop an approach to choice principles and their contrapositive bar-induction principles as extensionality schemes connecting an ''intensional'' or ''effective'' view of respe…
Realizability Interpretation and Normalization of Typed Call-by-Need -calculus With Control
Étienne Miquey, Hugo Herbelin
We define a variant of realizability where realizers are pairs of a term and a substitution. This variant allows us to prove the normalization of a simply-typed call-by-need $$λ…
Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant
Théo Zimmermann, Hugo Herbelin
In mathematics, it is common practice to have several constructions for the same objects. Mathematicians will identify them modulo isomorphism and will not worry later on which con…
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…
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.