Cut elimination in focusing with selection (M2) Automated CTL proofs in proof assistants (M1-M2) Combinaison des approches algébrique et "à la Hoare" : Preuve de concept (M2)