Proof assistants (M2 MPRI)