“I primarily worked on infinite proofs which is, philosophically, a novel way of proving things. A proof can be thought of as a debate between two people, one who is trying to establish the statement and the other who is trying to refute it. The statement has a proof if the person who is trying to prove it wins the debate.” Abhishek De, former PhD student at IRIF.
Link to his PhD thesis: Linear logic with the least and greatest fixed points. Truth semantics, complexity and a parallel syntax

I am Abhishek De, a postdoc student at the University of Birmingham. I obtained my Bachelor's and Master's degrees from Chennai Mathematical Institute (CMI). I did my PhD at Institut de Recherche en Informatique Fondamentale (IRIF) under the supervision of Alexis Saurin and obtained my doctoral degree in 2022. I work in logic, mostly on the structure of proofs.

I was bad at sports and relatively good at maths so I got into the olympiad circuit in high school. From then on, the path was almost predestined. I applied to all mathematics research institutes in my country with undergraduate programs and got into a few. Finally, I chose CMI because it had a dual degree in math and computer science. In undergrad, I realised maths was too difficult so I stuck to computer science. I did not have a favourite topic per se, I liked whichever topic was taught in an interesting fashion. My favourite teacher was R. Ramanujam, one of the most eminent logicians in the country, so I told him I wanted to work on logic. He sat with me, evaluated my interest and strengths, and advised me to apply to Alexis Saurin.

I primarily worked on infinite proofs which is, philosophically, a novel way of proving things. A proof can be thought of as a debate between two people, one who is trying to establish the statement and the other who is trying to refute it. The statement has a proof if the person who is trying to prove it wins the debate. Infinite proofs are debates which go on forever. My work on infinite proofs focused on canonical representations of infinite proofs called proof-nets. I also worked on the complexity (how hard is it to determine if a statement has an infinite proof or not) and semantics (the meaning of truth with respect to infinite proofs) of such systems.
Link to his PhD thesis: Linear logic with the least and greatest fixed points. Truth semantics, complexity and a parallel syntax

Fixed points are interesting computational gadgets. A recursive call in a program basically computes a least fixed point. A logical language that is expressive enough to talk about fixed points can express a lot of important things like “Eventually this client will be served” and so on. Consequently, the proof theory and model theory of logics with fixed points has been investigated with equal enthusiasm. While expressivity and complexity are the élan vital of the model-theoretic paradigm, axiomatisability is that of the proof-theoretic paradigm. Notwithstanding the particular style of writing proofs (i.e. Hilbert-style or sequent calculus or something else), there are three main approaches to the axiomatisation:

• emulating induction explicitly yielding finitary wellfounded systems
• construe fixed points as limit points of approximations yielding infinitely branching wellfounded systems
• emulating induction implicitly via self-reference yielding circular and non-wellfounded systems

Structurally, it's quite simple really: a non-wellfounded system is just a system of infinite trees. If we restrict to trees with finitely many subtrees, we have a circular system. The combinatorics of infinite trees are quite well-developed so the structural proof theory can oftentimes use Ramsey-like arguments implicitly or explicitly. However, things get complicated with the semantic and computational aspects. These proofs come with a progress condition that guarantees the absence of paradoxes and vicious circles. It is difficult to explain the progress condition denotationally since the science hasn't really gone beyond construing infinite proofs as infinite series of finite approximations (which are finite trees). On the computational side, infinite computations (like printing all prime numbers) correspond to the cut-elimination of infinite proofs which has been extremely difficult to be satisfactorily nailed down. My work on infinite proof-nets is a small step towards that goal.

There are two distinct strains of applications. Firstly, on the level of provability, fixed point linear logic is able to express several mathematical theorems and automated theorem provers that work on propositional fixed point linear logic could rival first-order theorem provers. Secondly, (and this follows from the previous question) via the Curry-Howard correspondence, (co)inductive data types correspond to fixed point formulas and (co)inductive programs correspond to circular proofs. Consequently, further research on infinite proofs (especially its computational aspect) can be applied in the design and evaluation of coinductive programs.

At the moment, I would like to throw a lot of mathematical tools at the cut-elimination of infinite proof-nets and see what sticks. In particular, the rewriting techniques of the Dutch school seem appealing. On a related note, I'm working on developing alternative styles of writing infinite proofs viz. natural deduction and deep inference. It would be interesting to see if the challenges thrown by the normalisation of these formalisms are similar to the ones I'm familiar with in the world of infinitary sequent calculus and proof-nets. Currently, I'm also involved in a project on providing a proof-theoretic solution to a problem in topological semigroup theory.