21 citations · 54 across the 7 of their papers we have counts for
9 papers
An analysis of the constructive content of Henkin's proof of Gödel's completeness theorem
Hugo Herbelin, Danko Ilik
G{ö}del's completeness theorem for classical first-order logic is one of the most basic theorems of logic. Central to any foundational course in logic, it connects the notion of va…
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…