Welcome
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.
Contact
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
News:
- 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.
Papers
Published articles
- 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).
Abstract accepted for presentations
- A formalisation of Hahn-Banach theorem in Coq , with Assia Mahboubi. Abstract accepted to TYPES
- Formalisation of Hahn-Banach theorem with the Mathematical Components Libraries + Axioms in Coq : code .
- Application Hahn-Banach theorem to normed spaces with the Mathematical Components Analysis libraries in Coq : code .
Thesis
- I defended my PhD thesis on October 19th 2018. You will find here the manuscript and the slides .
Formal Proofs
- How to install Coq, use Mathematical Components libraries, and formalise your favourite theorem advices (soon) .
Talks
Partial Differential Equations and Distributions in Linear Logic
- 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.
General introductory talks
- 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.
Internships
Education
- 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.