I'm a Post-Doc with Assia Mahboubi, at Inria Gallinette.

Here's a short CV (Oct. 19).

My research interests lie at the interface of Logic, Type Theory and Functional Analysis.

marie.kerjean[at]inria.fr

kerjean[at]irif.fr

Bureau 214

LS2N, premier étage Batiment 11 ,

UFR Sciences et Techniques

2, rue de la Houssinière,

44000 Nantes

France

- I'll be happy to supervise one intern during the spring/summer 2020. Here's an example of a submitted subject, but feel free to contact me for any subject about formal proofs in analysis or differential linear logic.
- Have you considered submitting to MFSP (deadline 09/01/2020) or SYCO (deadline 10/02/19) ?
- I am the beneficiary of a L'Oréal-UNESCO France Rising Talent Grant for the academic year 2019/2020.
- With Guilhem Jaber, we're organizing a reading group on differentiable programming.

- Chiralities in Topological Vector Spaces, 2019.

- Formalizing functional analysis structures in dependent type theory , with Reynald Affeldt, Cyril Cohen, Assia Mahboubi, Damien Rouhling and Kazuhiko Sakaguchi, accepted at IJCAR 2020.
- Models of Linear Logic based on the Schwartz ε-product, with Y. Dabrowski, 82 pages, 2020, published in Theory and Applications of Categories (journal).
- Chiralités et exponentielles: un peu de différentiation, with Ésaïe Bauer, JFLA 2019 (nationale conference)
- Higher-order distributions for Differential Linear Logic, with J.-S. Lemay, Fossacs 2019 (conference).
- A Logical Account for Linear Partial Differential Equations, 2018, LICS 2018 (conference).
- Mackey-complete spaces and power series - A topological model of Differential Linear Logic, with C. Tasson, 2018, Mathematical Structures in Computer Science (journal).
- Weak topologies for Linear Logic, 2016, Logical Methods for Computer Science (journal).

- A formalisation of Hahn-Banach theorem in Coq , with Assia Mahboubi. Abstract accepted to TYPES

- A deterministic differential lambda-calculus , 2016.

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

- How to install Coq, use Mathematical Components libraries, and formalise your favourite theorem advices (soon) .

- 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 , Cosynus Seminar, LiX, Palaiseau, February 2020.

- Higher-Order Distributions for Linear Logic , Invited talk to the Chocola Seminar , Lyon, November 2019.

- 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 , 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 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.

- 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.

- 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.

- 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.

- Master's thesis, under the direction of C. Tasson et PPS. Here are the slides. Beware of an error in the adaptation of Hahn-Banach's theorem.
- Report on the M1 internship, supervised by R. Blute at Ottawa's University.
- Report on the L3 internship, supervised by F. Wagner at the University of Lyon.

- 2014-2018 : PhD thesis under the direction of Thomas Ehrhard at IRIF, Université Paris Diderot.
- 2015- 2016 : Invited researcher in the PLS group at the IT University of Copenhagen
- 2013-2014 : Internship at PPS, under the direction of Christine Tasson.
- 2012-2013 : Master MPRI, Université Paris Diderot.
- 2011-2012 : First year of Master in advanced mathematics, ENS Lyon.
- June 2011 - July 2011 : Research Internship with F. Wagner, Université Lyon 1.
- 2010-2012 : B.Sc in advanced mathematics, ENS Lyon.
- 2007-2010 : Preparatory classes to Grandes Ecoles, Lycée Louis Le Grand, Paris.