Internship and PhD subject proposals
- 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)
