Lean for the Functional Programmer

Lean isn’t just an interactive theorem prover, it is also a general purpose functional programming language. In this tutorial, we will explore both sides of Lean by first fixing a bug in a small command line tool that filters JSON values, proving it correct, and then modifying both the program and the proofs to use efficient arrays instead of linked lists.

The tutorial is suitable for participants with some background in functional programming: we’ll assume a background with pattern matching, lists, and recursion, but we won’t assume any knowledge of advanced type system features.

The tutorial will be a mix of participants individually working on their own and all together helping the presenter. Therefore, we ask participants to check out the repository at https://github.com/david-christiansen/bob24 and follow the “Preparing for the Tutorial” instructions before Bobkonf.

Joachim Breitner

@nomeata

Ever since Joachim has found beauty and elegance in Functional Programming, he’s been working with and on functional programming languages, in particular Haskell, where he has contributed to the compiler, helps with the steering committee and is a co-host of the Haskell Interlude podcast.

He’s also always been fascinated by Interactive Theorem Proving and his academic persona used Isabelle and Coq for formalize mathematics and verify programs.

These two interests find their natural synthesis in the Lean programming language, and Joachim joined the Lean FRO to work on the lean compiler itself.

Besides such serious nerdery, you’ll find Joachim dancing Swing and Tango (in particular when traveling to conferences, so talk to him if you want to join), paragliding and unapologetically making bad puns.

David Thrane Christiansen

David Thrane Christiansen has worked with functional programming and dependent types in both academia and industry, with a particular interest in metaprogramming and domain-specific languages. He is the author of Functional Programming in Lean and, together with Daniel P. Friedman, The Little Typer. David works full-time at the Lean FRO on making the process of writing and maintaining documentation as easy as possible. Before working at the Lean FRO, he was the Executive Director of the Haskell Foundation, and he has multiple years of industrial Haskell experience at both Deon Digital and Galois. Before that, David contributed extensively to the first version of Idris.