“Generally, I am interested in mathematical logic (proof theory) and its connections with Algebra through semantics. This is what I have done in my thesis for a specific logic.” Farzad Jafarrahmani, former PhD student at IRIF.

Link to his PhD thesis: Fixpoints of Types in Linear Logic from a Curry-Howard-Lambek Perspective

My name is Farzad Jafarrahmani, I grew up in Qazvin, Iran. In 2012, I started my bachelor at Sharif university of Technology, Tehran via a national competition, called Concours. At the beginning, I chose three different trainings in order of priority: 1) Physics 2) Computer Science 3) Mathematics. My grades were too low to be accepted for Physics, so I started studying computer science. I obtained my bachelor with a double degree training in computer science and mathematics in 2017. I continued with a master in the MPRI (Master Parisien de Recherche en Informatique) program at Ecole normale supérieure de Cachan. In 2018, I did one of my internships at IRIF under the supervision of Thomas Ehrhard. In 2019, Thomas Ehrhard and Alexis Saurin (IRIF) graciously accepted me as a PhD student.

I was always so keen to think and understand mathematical problems, especially on geometry. This interest seriously started by attending the Mathematics Olympiad when I was 13 years old. During my bachelor degree, I was curious to know how I can write articles in the field of geometry. My professor Alireza Bahraini kindly directed me to some books on Algebraic geometry which were hard for me to understand. When I saw mathematical logic applied for the first time in a general math course given by Rasoul Ramezanian, I was even more curious for other references in mathematical logic and especially on intuitionistic logic. What was interesting in those references was how mathematicians solve problems, the functionality of the human brain. From now on, I knew I wanted to develop a machine (computer) to compute the probability of being true or false of a mathematical conjecture. I thought this is related to the field of biological mathematics so I attended a journal club in cognitive science at the Institute for Research in Fundamental Sciences (IPM) in Tehran. My curiosity for this subject led me to do two research internships with Joxan Jaffar and Anthony Widjaja Lin at the National University of Singapore and Yale-NUS College in summer of 2015 and 2016, and I also worked remotely for two years (2015-2016) with Yuanlin Zhang in Texas Tech University. I finally finished my bachelor thesis on the relation of algebra (ordered field) and mathematical logic under supervision of Mohammad Gholamzadeh Mahmoudi. Now, I feel that my PhD topic was really close to what I always was interested into. I was so lucky to meet the right people during this path, and I am so thankful to all the people and friends that helped me a lot during my studies and research.

Generally, I am interested in mathematical logic (proof theory) and its connections with Algebra through semantics. And this is what I have done in my thesis for a specific logic. This logic that I focused on is an extension of linear logic with fixed points operator.

What I understand intuitively from Curry-Howard-Lambek correspondence is that it creates a correspondence between three areas of mathematical logic, computation theory, and mathematics. This started first by Curry-Howard correspondence which says how we can obtain a computational point of view on mathematical logic, and then it extended to Curry-Howard-Lambek correspondence to see that notion of computation as some concrete objects of mathematics.

MULL is that specific logic that I mentioned above, extension of linear logic with fixed point operator. By categorical semantics of MULL, I mean looking at MULL from a Curry-Howard-Lambek perspective. That intuitively means that we tried to relate this logic (MULL) to the objects of the mathematics world, and also studying computational behavior of that logic.

In a broad sense, what we did can have applications in the field of programming languages. What I understand is that developing a programming language can be a very complicated job, as usually there are many different options to implement an idea or a property. So, the first question is how the developer should decide between those different options. This question is what I call the syntactical question. One way to answer the question is to try to abstract the required property in a formal language, and translate those different options in that language as well. And then see what kind of information one can obtain by studying the syntactical question in that formal language. And why not consider mathematics as that formal language? So, if one wants to implement MULL in a programming language, the first question can be the syntactical question.

I am actually continuing what I started in my PhD. I am currently doing a postdoc at the Sorbonne Université in the LIP6 laboratory, and working on similar subjects to my PhD.