This project is a grouping of three teams (2 INRIA, 1 foreign) through their common belief in the need for a new way of looking at syntax in proof theory. On one side, syntax is a blessing, because it is the handle that algorithms can work on. On the other side it is a curse because it comes with bureaucracy that disguises the essence of proofs and very often causes unnecessary exponential blow-up in the complexity of proof search. We intend to tackle the problem of bureaucracy by using approaches based on proof nets, which are intrinsically bureaucracy-free; on deep inference, which allows to design deductive systems with reduced bureaucracy; on focussing, which tells us how to reduce the search space during proof search; and on games semantics, which provides new computational models for proof search. The close relation between these fields has been revealed only within the last few years, and we plan to further unify them.
There is also a poster and a two-slide presentation.
Within the project we have a 12-month postdoc position at LIX which is being filled by Tom Gundersen. (Details can be found here.)