Charleston Lean Proof Assistant Meetup

Lean is a functional programming language with a highly expressive type system. It can be used to produce performant programs that are guaranteed to meet their specifications, which proves that a large class of bugs cannot exist in your program. It can also be used to interactively prove theorems in mathematics. This meetup is for enthusiasts to join together to learn, code, and share their experiences with Lean.

Like last time, our next meeting will be split into two parts. Jared will talk about using Lean as a function programming language. Ben will review the article "Perceus: Garbage Free Reference Counting with Reuse" that introduces the novel programming paradigm FBIP (Functional But In-Place)