Welcome

I am a CNRS researcher in the Love team at the LIPN.

Previously, I was post-doc with Assia Mahboubi, at Inria Gallinette. Before that, I did my PhD thesis at the IRIF, under the direction of Thomas Ehrhard.

Here's a short CV.

My research is motivated by the gap between the theory programming languages and the applications of programming languages to continuous mathematics. It lies at the interface of Logic, Formal Proofs and Functional Analysis. I am a happy participant to the Math-Comp Analysis project. I am a member of the ANR ∂IFFERENCE (starting in 2020) and Nuscap (starting in 2021).

Contact

• kerjean[at]lipn.fr
• Office A 212 -
  LIPN, Institut Galilée – Université Paris 13
  99, avenue Jean-Baptiste Clément 93430 Villetaneuse

News:

• Simon Mirwasser is starting his PhD on Differential Linear Logic indexed by Differential Operators (september 2022).
• Our abstract on copromotion in collaboration with Jean-Simon Lemay was accepted to the TLLA20022 workshop.
• I am part of the CPP 2023 program committee. Please consider submitting your paper (deadline: Sep 21, 2022 )!
• I will give an invited talk to the Wollic 2022 workshop in september.
• I am part of the TLLA 2022 program committee. Do not hesitate to send an abstract (deadline: May 20th)!
• I gave a talk at the CIRM LL winter school .
• I gave an invited talk at the AIPLANS workshop, colocated with NeurIPS 2021, on Dec. 14th.
• Jean-Simon Pacaud Lemay came to the LIPN lab for a 10 day research visit (october 2021).
• Valentin Maestracci started a 6 month internship on *-autonomous differential categories (October 2021).

Students and Interships

I am always happy to work with students. If you have a taste for logic and love to open analysis books, please do not hesitate to contact me ! I'm also happy to supervise formalizations projets in Coq.

Papers

Preprints

• Chiralities in Topological Vector Spaces , 2019. preprint
• ∂ is for Dialectica, with Pierre-Marie Pédrot , 2021. preprint .

Published articles

• Competing inheritance paths in dependent type theory: a case study in functional analysis, with Reynald Affeldt, Cyril Cohen, Assia Mahboubi, Damien Rouhling and Kazuhiko Sakaguchi, accepted at IJCAR 2020 (conference). preprint


• Models of Linear Logic based on the Schwartz ε-product, with Yoann Dabrowski, 82 pages, 2020, published in Theory and Applications of Categories (journal). preprint .


• Chiralités et exponentielles: un peu de différentiation, with Ésaïe Bauer, JFLA 2019 (national conference). preprint


• Higher-order distributions for Differential Linear Logic, with Jean-Simon Lemay, published at Fossacs 2019 (conference). preprint.


• A Logical Account for Linear Partial Differential Equations, 2018, LICS 2018 (conference). preprint


• Mackey-complete spaces and power series - A topological model of Differential Linear Logic, with Christine Tasson, 2018, Mathematical Structures in Computer Science (journal). preprint


• Weak topologies for Linear Logic, 2016, Logical Methods for Computer Science (journal). paper

Popularization

• A popularization article on formal proofs and semantics in Blog Binaire .

Thesis

• I defended my PhD thesis on October 19th 2018. You will find here the manuscript and the slides .

Talks

Formal Proofs

• Complex Analysis through a hierarchy of real analysis structures , Lean Together 2021.
• A formal Classical Proof of Hahn-Banach Theorem , BigProof 2019 Workshop, Edimburgh, May 2019.
• A formal Classical Proof of Hahn-Banach Theorem , TYPES 2019, Oslo, June 2019.

Typing differentiable programming

• ∂ is for Dialectica , SEMINÁRIO DE LÓGICA MATEMÁTICA, Lisboa, Online, March 2022.
• ∂ is for Dialectica , Invited talk to the Chocola Seminar, Lyon, March 2022.
• ∂ is for Dialectica , Mathematical Foundations Seminar, Bath, Online, November 2021.
• ∂ is for Dialectica , TLLA 2021, Online Workshop, Invited Talk, June 2021.
• Typing differentiable programming , LoVe Team Seminar, LIPN, April 2021.
• Typing differentiable programming , Cosynus Team Seminar, LiX, Palaiseau, February 2020.

Distributions in Linear Logic, polarized models

• Differential Linear Logic extended to differential operators , Invited short talk to the Linear Logic Winter Schoool, CIRM, Marseilles, January 2022.
• Higher-Order Distributions for Linear Logic , Invited talk to the Chocola Seminar , Lyon, November 2019.
• Higher-Order Distributions for Linear Logic , Contributed talk to FoSSacs 2019, Prague, April 2019.
• Differentiating proofs and programs , Invited talk at SYCO3, March 2019.
• A logical account for LPDEs , Higher Order Models of Differential Linear Logic, given at Bellairs Workshop in March 2019.
• A logical account for LPDEs , Seminar given at the LIX, Polytechnique, November 2018.
• A logical account for LPDEs , Contributed talk to LICS 2018, Oxford, JuLy 2018.
• A logic for LPDEs , Invited talk to a special session, Conference MFPS 2018, Halifax, Canada, June 2018.
• A Type Theory for Linear Partial Differential Equations , Poster for the Annual days of the GDR-IM, Ecole Polytechnique, April 2018.
• A Type Theory for Linear Partial Differential Equations, Antique team, ENS Ulm, Paris, March 2018.
• Smooth models of linear logic and Partial Differential Equations , Journées GEOCAL-LAC, Nantes, November 2017.
• Smooth models of linear logic and Partial Differential Equations , Seminar of the team LCR, LIPN Université Paris 13, November 2017.
• Smooth differential linear logic and Partial differentials equations , Trends in Linear Logic and Applications, Oxford, September 2017.
• Smooth models of Linear Logic : Towards a Type Theory for Linear Partial Differential Equations , Seminar Chocola, Lyon 2017, June.
• Towards a Type Theory for Linear Partial Differential Equations , PLS group, ITU Copenhagen, June 2017.

Models of LL based on the Schwartz epsilon product

• Models of LL based on the Schwartz epsilon product , Contributed talk to TLLA 2018, Oxford, JuLy 2018.
• Models of LL based on the epsilon product, an introduction to LL , joint work with Y. Dabrowski, séminaire de géométrie et physique mathématique, Paris Diderot, May 2018.
• Smooth models of linear logic , Seminar of the LIMD team, LAMA, Université Savoie Mont Blanc, Chambéry, December 2017.
• Smooth models of linear logic , Forum des jeunes mathématicien.ne.s, Nancy, 2017.
• Smooth models of Linear Logic based on the Schwartz' epsilon product , Second General Meeting of the GDRI-LL , Roma, October 2017.
• Smooth models of Differential Linear Logic , DIKU, Copenhagen, June 2017.

Mackey-Complete spaces as a quantitative model of DiLL

• Mackey-complete spaces and power series : a topological model of Differential Linear Logic , Workshop QSLC, September 2016.
• A poster , prepared for the Journées nationales 2016 du GdR IM , Januray 2016.
• Complete spaces and Differential Linear Logic, GDT sémantique, PPS, June 2013.

Deterministic Differential Lambda calculus

• The computational meaning of differentiation, PLS group Seminar, ITU Copenhagen, November 2015.
• Reduction strategies for the differential lambda-calculus, Géocalisation Summer school, Chambéry, June 2015.

Weak topologies for Linear Logic

• Tensor Product and *-autonomous categories, TACL 2015 (peer reviewed conference), Ischia, June 2015. The abstract.
• Weak topologies for Linear Logic , LDP séminar, Marseille, January 2014.
• Weak topologies for Linear Logic Workshop SD14 (peer-reviewed workshop), Vienna, July 2014. The abstract.

General introductory talks

• Computing Analysis through Logic , Invited tutorial to the workshop on Tangent Category and Applications, BIRS, Calgary, June 2021 [video].
• Computing Analysis through Logic , a poster prepared for prize-giving ceremony L'Oréal Unesco 2019.
• Differential Linear Logic , Doctoral course on the semantics of linear logic, Copenhagen, February 2016.
• Linearity and Differentiation,PhD' Student' Semainar, LIAFA and PPS, Paris, November 2013
• Logique Linéaire et Analyse fonctionnelle, 13th forum for young mathematicians, Lyon, November 2013.