4 papers
Retro-synthetic Riemannian geometry in Rocq I : Taylor series of a metric
Gabriella Clemente, Hugo Herbelin, Carlos Simpson
We introduce a synthetic framework for doing local Riemannian geometry that is influenced by a reverse-engineering method for formalizing in Rocq. These new perspectives and techni…
Proving and Computing: The Infinite Pigeonhole Principle and Countable Choice
Zena M. Ariola, Paul Downen, Hugo Herbelin
Structural recursion is a common technique used by programmers in modern languages and is taught to introductory computer science students. But what about its dual, structural core…
The very dependent recursive structure of iterated parametricity in indexed form
Hugo Herbelin, Ramkumar Ramachandra
Reynolds' parametricity originally equips types with proof-irrelevant binary propositional relations over the types. But such relations can also be taken proof-relevant or unary, a…
On the logical structure of some maximality and well-foundedness principles equivalent to choice principles
Hugo Herbelin
We study the logical structure of Teichm{ü}ller-Tukey lemma, a maximality principle equivalent to the axiom of choice and show that it corresponds to the generalisation to arbitrar…