Here is a list of internships topics that I propose. The difficulty of the internships
is variable :
- (L3-M1) Instrumentation of a Geological Simulation Tool (in C++). More information (in French)
in this file.
- (M2) Translations between two DSL applied to (digital twins) model description.
More information (in French)
in this file.
- (M2) Optimized double-negation translations in Dedukti. The idea is to let negation be operators
that are formula transformers, in the spirit of Gilbert's thesis. More information
in this file.
- (L3-M1-M2) 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.
- (M2) 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.
Here is a list of PhD offers.
- there are opportunities at EDF R&D, the French National Electricity company, for
academic-industrial subjects around the use of domain-specific languages to describe
physical models and simulations. Please contact us if you are interested.
- A categorical model of a higher-order logic with constraints : the target logic is a
logic where (first-order) constraints are used to express generalized terms instead
of terms of a higher-order logic. The model theory of this logic is a wide area of
investigation that will lead to generalization of previous (categorical or not) semantics
for higher-order logic. In collaboration with Pr. Jim Lipton at Wesleyan University.
- 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.