—ITP'26, part of FLoC'26—Functional correctness of an optimized modular inversion algorithm (paper) (slides)
—RocqPL'26—Automatic generation of parametricity translations for inductive types at RocqPL'26 (abstract) (slides)