Le site web de Dominique Cansell
http://dominique.cansell.free.fr/ I officially stopped my research more than 15 years ago but I worked sometime with Jean-Raymond Abrial when he was stuck in a proof or a development. In 2017 JRA asked me to work on the Goodstein sequence (ordinals) In 2019 we worked on a Protocop inspired by the Lamport's Paxos one. This work will be presented in ABZ2025 the original paper Rodin archive for the direct approach Rodin archive for the constructive approach JRA's Profile using PP and SMT End of 2020 JRA asked me to work on his new instantiation (component). I think it's a good thing and I've use it to develop many context and theorems. This work was done in the EBRP ANR project my EBRP activity I am retired in march 2025 and my unique objective is to propagate JRA's ideas.