3 papers
cs.PL2026
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…
cs.LO2026
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…
cs.LO2024
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 arbitra…