• Term transformation and proof (re)construction (L3-M2)
• Translating Lean to Dedukti (M1-M2)
• Developping a standard library for Lambdapi (L3-M1)
• Concept alignment in Logipedia (M1-M2)
• Classical proofs in Logipedia (M1-M2)
• 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)