Paris area, France

Stream: Geographic locality

[Samuel Lelièvre]

I'm in Orsay, Paris area, France.

[Patrick Massot]

I'm also there, we should be able to meet after the lock-down!

[Patrick Massot]

(Samuel is working in my math department).

[Etienne.bfx]

Hi, I am a first year PhD student in Ergodic Theory and Hyperbolic geometry. I am at Ecole polytechnique, a school near Paris.

[Kunhao Zheng]

Hi! I didn't find the stream before! I'm also from EP and I'm doing my 3A internship right now. Enchanté!

[Floris van Doorn]

I'm starting to work with @Patrick Massot this week at the University of Paris-Saclay.

[Filippo A. E. Nuccio]

Welcome to France, @Floris van Doorn !

[Frederic Peschanski]

Bonjour, I'm an associate professor at Sorbonne University (campus Jussieu) in theoretical computer science and combinatorics.

[Kyle Miller]

I recently started working with @Patrick Massot at Université Paris-Saclay, sharing an office with @Floris van Doorn

[Rish Vaishnav]

I have recently joined the LMF at Université Paris-Saclay! I will be working on designing and implementing a translator between Lean and Dedukti (and on proof system interoperability more generally).

[Patrick Massot]

Nice! We have a very informal seminar where people interested in formalized maths try to meet once every two weeks in Orsay. I wrote "try" because sometimes we don't manage to meet (especially in those days when a stubborn government insist on a very unpopular pension system reform, resulting in many days where protests make it very difficult to move in the Paris area). Do you want to receive information about it? Ideally you could even give a talk so that we get to know you. It doesn't matter whether you formalized great stuff or not, you could simply tell us what you are interested in.

[Rish Vaishnav]

Yes, I would love to attend and introduce myself! Feel free to add me to any relevant mailing list.

[Sam van G]

Me too, please, @Patrick Massot. Thank you!

[Sam van G]

I think I never introduced myself here: I am an associate professor ("maître de conférences") at IRIF, Université Paris Cité.

[Yvon Fredrich]

Hi, I'm a maths student at the ENS paris saclay and curious about mathlib, lean and all the interfaces aroud lean. I'm still very new though. I'm also interested in the informal seminar in Orsay @Patrick Massot, could I receive information about it ?

[Riccardo Brasca]

For those around, I will give a talk next Monday, at 2023-03-20T14:00:00+01:00 or 2023-03-20T15:00:00+01:00 (still to be confirmed) about the flt-regular project. The talk will be at Université Paris Cité (aka Paris 7, aka Paris Diderot, aka Université de Paris...), here

It will be quite similar to my last year talk at Orsay.

[Nicolas Rolland]

Bonjour, I am interested in using Lean as a programming language and DSL host, relying on category theoretical constructs (mostly distributors from Jean Bénabou)

[Riccardo Brasca]

Welcome! Where are you based? In Paris area there are mostly mathematicians interested in Lean, but we are happy to get new people involved!

[Nicolas Rolland]

In Paris indeed ! The ability to express both (categorical) math and real programs in the same language is very enticing and will hopefully be fruitful

[Nicolas Rolland]

btw, I (used to) organize a functional programming meetup group in Paris and plan to reboot it, if only to talk about Lean . It is a perfect ground for making presentations talks to a forgiving audience, (mostly) amateur in formal methods, haskell/ml/scala practionners . It can be useful to evangelize Lean (hence my desire to reboot it), to polish and practice presentations before going to your peers for hard scrutiny, or to showcase "programming pearls" you find useful. It is more "program" inclined than mathy, but they were happy to hear about monoidal string diagrams and monads

[Shreyas Srinivas]

If it is online, I would love to join. I am 2-3 hours from Paris, but it costs 100 Euros to get there

[Riccardo Brasca]

For those around Paris this should be interesting (I think it is more for students than experts, but still)

[Vincent KUBICKI]

Hi, I am completely new to proof assistant. I am an amateur who wants to understand the jump from functional language (Haskell) to theorem proving. I live and work in Lille in ML / IA (mostly in C++).

[Patrick Massot]

Welcome! Isn't it risky to publicly write that Lille is in the Paris area?

[Vincent KUBICKI]

1 hour of TGV, come on :).

[Ruben Van de Velde]

Lille? That's nearly Belgium!

[Vincent KUBICKI]

There is a beautiful part of Flanders on this side of the border also.

[Patrick Massot]

I'm leaving. I don't want to be around when someone from Lille comes here and start killing everyone without trying to figure out who said Lille is in the Paris area and who said it is in Belgium.

[Filippo A. E. Nuccio]

Oh, I thought it was in Canada... :angel: :flag_canada: