Portland, OR

Stream: Geographic locality

[Joe Hendrix]

Galois is pretty regularly using Lean in Portland.

[Aaron Anderson]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

There's a little information here which I found interesting

[Joe Hendrix]

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]

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

[Joe Kiniry]

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.

[Adam Layne]

There is a newly-formed Portland Haskell meetup: https://www.meetup.com/portland-has-skill/

Many of us have experience with/use Lean and other dependently typed languages and they come up in conversation a lot.

[Max Nowak 🐉]

I'm in Portland until January, doing some semantics of imperative languages. Would love to meet some fellow Lean addicts :D. I'll likely go to the Portland Has Skill meetup tomorrow.