Welcome

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

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:

• With Guilhem Jaber, we're organizing a reading group on differentiable programming.
• I am the beneficiary of a L'Oréal-UNESCO France Rising Talent Grant for the academic year 2019/2020.
• Did you consider submitting to LAFI ?

Papers

Submitted

• Models of Linear Logic based on the Schwartz ε-product , with Y. Dabrowski, 82 pages.

Published articles

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

In preparation

• Polarization in topological vector spaces, based on Chapter 6 and Chapter 2.5 of my thesis

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

Teaching - Enseignements

Talks

Formal Proofs

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

Partial Differential Equations and Distributions in Linear Logic

• 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

• 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

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

Education

• 2014- : 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. Rank 6/41.
• June 2012 - July 2012 : Research Internship with R. Blute, University of Ottawa.
• 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.