Showing cs.LOShow all
2 papers · 1 filter
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 arbitrar…