Gothenburg, Sweden

Stream: Geographic locality

[Victor Ahlquist]

Studying for a B.sc in maths at the University of Gothenburg. Trying to learn Lean in my spare time, hopefully I'll be good enough to contribute to mathlib in time.

[Jannis Limperg]

Hej! If you're interested in type theory more broadly, check out the Initial Types Club at Chalmers. It's a weekly-ish undergrad-friendly seminar on type theory and adjacent topics (or at least it was when I was there).

[Victor Ahlquist]

Thanks for the link. Unfortunately I'm more interested in the mathematical side of Lean rather than the type-theoretic, but I might check it out in the future if my tastes have changed :)

[Jannis Limperg]

I'll allow it. But be aware that this is all an elaborate scheme for generating type theory PhDs. :octopus:

[Kevin Buzzard]

It's supposed to be an elaborate scheme for getting mathematicians interested in theorem provers!

[Mario Carneiro]

Starting today, I am now officially starting my new postdoc at Chalmers University under Magnus Myreen, after finishing my postdoc at CMU under Jeremy Avigad. I don't have any specific projects I've come here to do, but expect some Lean/CakeML crossovers soon!

[Shreyas Srinivas]

Nice!! Will we see a deep embedding of cake ML in lean soon?

[Mario Carneiro]

actually yes, that's one of the near term projects we talked about today, Magnus was already planning on doing something like that for Coq and doing it for lean instead or in addition should be not hard

[Shreyas Srinivas]

Is the plan to implement the proof producing front end alone? I toyed with the idea during my vacation and put it aside because I didn't know how to represent non-terminating programs

[Shreyas Srinivas]

(deleted)

[Mario Carneiro]

not proofs, just the semantics of CakeML

[Mario Carneiro]

the idea is so that you can prove the correctness of CakeML programs in lean

[Mario Carneiro]

so kinda like using VST and then trusting CompCert

[David Thrane Christiansen]

@Mario Carneiro You're not that far away - if you ever pass through CPH, drop me a line