Zulip Chat Archive

Stream: Geographic locality

Topic: Portland, OR

Joe Hendrix (Jun 27 2020 at 04:05):

Galois is pretty regularly using Lean in Portland.

Aaron Anderson (Jun 28 2020 at 17:40):

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

Bhavik Mehta (Jun 28 2020 at 17:43):

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

Bhavik Mehta (Jun 28 2020 at 17:43):

There's a little information here which I found interesting

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.

Joe Hendrix (Jun 29 2020 at 21:56):

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

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: Dec 20 2023 at 11:08 UTC