Tutorial Speaker Leonardo de Moura
Leonardo de Moura is a Senior Principal Applied Scientist in the Automated Reasoning Group at AWS. In his spare time, he dedicates himself to serving as the Chief Architect of the Lean FRO, a non-profit organization that he proudly co-founded alongside Sebastian Ullrich. He is also honored to hold a position on the Board of Directors at the Lean FRO, where he actively contributes to its growth and development. Before joining AWS in 2023, he was a Senior Principal Researcher in the RiSE group at Microsoft Research, where he worked for 17 years starting in 2006. Prior to that, he worked as a Computer Scientist at SRI International. His research areas are automated reasoning, theorem proving, decision procedures, SAT and SMT. He is the main architect of several automated reasoning tools: Lean, Z3, Yices 1.0 and SAL. Leonardo de Moura’s work in automated reasoning has been acknowledged with a series of prestigious awards, including the CAV, Haifa, and Herbrand awards, as well as the ACM SIGPLAN Programming Languages Software Award twice for Z3 and Lean. His work has also been reported in the New York Times and many popular science magazines such as Wired, Quanta, Nature News, and Scientific American.
Talk
The Lean Programming Language and Theorem Prover
Time: TBA
Room: TBA
Lean is a general-purpose programming language and interactive theorem prover developed by the Lean Focused Research Organization (Lean FRO). It has gotten much attention as the basis for the vast mathematical library (mathlib) and successes in formalizing contemporary research mathematics, but as a general purpose system, it can also be used for authoring and verifying software among other applications. In this tutorial you will get a feeling for typical use of Lean for computer scientists: We will define a deep embedding of a simple imperative language, use Lean’s flexible frontend to give it custom syntax, define semantics and finally prove simple optimizations as well as concrete programs correct.