Here is a list of internships topics that I propose. The difficulty of the internships
is variable.

- (internship/PhD) Polarized Deduction Modulo Theory: implementation and proof theory of
Polarized Deduction Modulo Theory, a framework that combines inference rules
with
*specialized* rewriting. Both in a first-order automated
theorem prover
(Zenon Modulo)
and in a more advance type theoretic tool
(Dedukti).
More information in
this file.
Parts of this ambitious project, e.g. implementation,
can also be proposed as internships.
- (internship) Maude in Dedukti: defining an embedding of Rewriting Logic inside Dedukti,
and compare with Maude, that natively supports Rewriting Logic. More information
in this file.
- (internship) Normalization by Completeness: explore the links between normalization proofs in
natural deduction (for instance those based on reducibility candidates arguments)
and semantic cut admissibility proofs. More information
in this file.
- other L3/M1 topics on demand. For instance: syntactic completeness proof for intuitionistic tableaux methods.