—‘Functional correctness of an optimized modular inversion algorithm’ at ITP'26, part of FLoC'26 (paper) (slides)
—‘Functional correctness of an optimized modular inversion algorithm’ during a visit to the STAMP team (slides)
—Automatic generation of parametricity translations for inductive types at RocqPL'26 (abstract) (slides)