email: [farzadhtg] at gmail.com, [farzad.jafarrahmani] at huawei.com
Physical address: Centre-Lagrange, 103 Rue de Grenelle, 75007 Paris.
Since April 2024, I am a researcher in Lagrange Mathematics and Computing Research Center (LMCRC), Huawei.
Previously, I was a postdoctoral researcher at LIP6 working with Christine Tasson and Adrien Guatto. And before all that and since October 2019, I was a PhD student in Computer Science at IRIF laboratory advised by Thomas Ehrhard and Alexis Saurin.
I am interested in proof theory and its connections with Algebra through semantics.
I will give lectures on basics of category theory and denotational semantics of (co)inductive types and fixed-point logics at EPIT 2025.
I will give a talk at IMS 2024 (International Mathematics Competition for University Students). The slides are here, and the homework is here.
I gave a talk in MFPS 2024 in the session on the semantics of non-wellfounded and circular proofs. Here is the link.
I will be defending my PhD on the 25th of January 2023. More information can be found here.
From May 2022 to July 2022, I will be a visiting researcher at the Computer Laboratory, University of Cambridge, working with Marcelo Fiore.
We're organizing a reading group on fixed point and circularity in proof theory.
Conferences paper:
On the denotation of circular and non-wellfounded proofs in linear logic with fixed points. With Thomas Ehrhard and Alexis Saurin. To appear in LICS 2025.
Fixpoint constructions in focused orthogonality models of linear logic. With Marcelo Fiore and Zeinab Galal. MFPS 2023. Arxiv.
Phase Semantics for Linear Logic with Least and Greatest Fixed Points. With Abhishek De and Alexis Saurin. FSTTCS 2022.
Categorical models of Linear Logic with fixed points of formulas. With Thomas Ehrhard. LICS 2021. HAL.
Unpublished Work:
Polarized linear logic with fixpoints (technical report). With Thomas Ehrhard and Alexis Saurin.
On relation between totality semantic and syntactic validity. With Thomas Ehrhard and Alexis Saurin. TLLA 2021. HAL.
On the denotational semantics of Linear Logic with least and greatest fixed points of formulas. With Thomas Ehrhard. HAL (2019).
Thesis manuscripts:
PhD: Fixpoints of Types in Linear Logic from a Curry-Howard-Lambek Perspective.
Master 2: Induction in the Fibred Multicategory. Supervised by Noam Zeilberger and Gilles Dowek.
Master 1: Denotational semantic of linear logic with least and greatest fixpoint. Supervised by Thomas Ehrhard.
B.Sc thesis (in Persian): Formally real fields and an application of model theory in Hilbert's seventeenth problem. Supervised by Mohammad Gholamzadeh Mahmoudi.
Grammaire et analyse (2023-2024) at Université Paris Cité.
Automates et analyse lexicale (2023-2024) at Université Paris Cité.
Compléments de programmation orientée objet (2023-2024) at Université Paris Cité.
Discrete mathematics (2020-2021, 2021-2022, 2022-2023) at ENS Paris-Saclay
Java Programming (2019-2020) at École Polytechnique.
Architecture+Systems (2020-2021) at ENS Paris-Saclay
