Internships

Here are possible internship topics for an M1 student. Don't hesitate to contact me if you have any question, either scientific practical. Internships would take place at ITU Copenhagen where I'm about to move.

Proof theory and Büchi automata

Büchi automata are commonly used in verification: infinite behaviors and specifications on such behaviors may be expressed as automata, so that the program satisfies its specification when its automaton is included in the specification's automaton. One may then forget about logic and focus on designing efficient algorithms for analyzing automata. It is however desirable that the inclusion-checking algorithm returns a certificate that can be independently and easily checked. Better, one may hope that this certificate corresponds to a proof in a larger framework, usable as part of complex formalizations involving a mix of automated and interactive proof development.

We are thus interested in revisiting automata-theoretic results from the viewpoint of logic, and more precisely proof-theory. Earlier work on finite automata illustrates that this is an interesting non-trivial program: although formalizing existing techniques is in principle feasible, we seek a more direct understanding which may require new notions. This kind of approach promises to be very instructive both from the viewpoint of automata theory and that of studying of (co)inductive proofs.

Term equality in proof theory and proof search

Deciding whether a logical statement holds may be done directly by enumerating (a complete subset of) proofs, when the considered logic has good enough proofs. This idea has driven a generalization of logic programming, leading to the notion of uniform proof, further refined into focused proofs, which bring a very rich proof-theoretic foundation not only for logic programming but more generally for theorem proving.

In that perspective, it is desirable to adopt strong notions of equality that directly reflect assumptions on terms, thanks to an elimination rule which enumerates complete sets of unifiers. Despite successes of that approach, it also comes with a few hard problems. In particular, unification is undecidable in many term languages, and decidable fragments are typically not closed under substitution, so that simple proofs may become arbitrarily complex or even unfeasible when we instantiate them. In the end, the feasibility of a proof may depend on the order of application of equality rules, a phenomenon that currently escapes proof-theoretic analysis. A recent refinement of the equality rule eliminates some of those problems, but it also complicates proof search a lot. The purpose of this internship is to study the structure of proofs using such a rule in various more or less simple fragments, in order to obtain complete classes of proofs, and try to gain some insight about proof search.