@jevonduve presents AlgoLean, a library that lets you formalize algorithms and reason about their runtime complexity in Lean, by representing them as Free Monads
Join us at the SF Lean Meetup! (sflean dot group)
Video
AlgoLean is a Lean library that formalizes algorithms and enables reasoning about…
Brief
AlgoLean, presented by @jevonduve, is a Lean library that models algorithms as Free Monads to let users specify and prove runtime-complexity properties inside Lean. The talk was shared with the SF Lean Meetup community and a recording/video is available; meetup details at sflean.group.
Why it matters
AlgoLean is a Lean library that formalizes algorithms and enables reasoning about their runtime complexity by representing algorithms as Free Monads.
Key details
- Presentation by @jevonduve was shared with the SF Lean Meetup community; video and meetup info available via sflean.group.