Zulip Chat Archive

Stream: Geographic locality

Topic: Portland, OR


view this post on Zulip Joe Hendrix (Jun 27 2020 at 04:05):

Galois is pretty regularly using Lean in Portland.

view this post on Zulip Aaron Anderson (Jun 28 2020 at 17:40):

As a pure mathematician, I hate this question... but what on earth for?

view this post on Zulip Bhavik Mehta (Jun 28 2020 at 17:43):

https://leanprover.github.io/talks/LeanAtGalois.pdf

view this post on Zulip Bhavik Mehta (Jun 28 2020 at 17:43):

There's a little information here which I found interesting

view this post on Zulip Joe Hendrix (Jun 29 2020 at 21:55):

The main current project I'm working on is a mouthful a "verified verification condition generator for a decompiler", namely one I worked on for decompiling x86 to LLVM.

view this post on Zulip Joe Hendrix (Jun 29 2020 at 21:56):

I previously worked on verifying aspects of a hash-based distributed timestamping service.

view this post on Zulip Joe Kiniry (Apr 30 2021 at 21:48):

Hey @Joe Hendrix. I have arrived here. I decided to play with porting some of my formalization of SysMLv2 from PVS to Lean for fun.


Last updated: May 09 2021 at 23:10 UTC