Charleston Lean Proof Assistant Meetup

Beginner
SUMMARY

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.

In this first meeting, we will focus on getting to know the people interested in the Charleston area and work through a Lean tutorial together.

WHAT YOU WILL LEARN
  • How to get Lean installed in VS Code.
  • How to interact with Lean to state and prove basic statements.
  • What are dependent types.

ABOUT THE HOST
Jared CorduanOperating Systems Engineer, BigBear.ai
VITALS

COST

NO FEE

DURATION

2 hrs

CLASS SIZE

40 persons

LOCATION

4 Conroy St, Ste A
Charleston, SC 29403

PHONE

(843) 972-7666, ext 2

EMAIL

info@charlestonlc.org