Leonardo de Moura
The Lean Theorem Prover
April 6, 2016 at 3:30pm
CSE 203
Abstract
Lean is a new open source theorem prover being developed at Microsoft Research and Carnegie Mellon University, with a small trusted kernel based on dependent type theory. It aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs. Lean is an ongoing and long-term effort, but it already provides many useful components, integrated development environments, and a rich API which can be used to embed it into other systems. It is currently being used to formalize basic datatypes and algebraic structures, a library for homotopy type theory, rudimentary category theory, and analysis. In this talks we describe the project goals, system architecture, and main features.
Bio
Leonardo de Moura is a Principal Researcher in the RiSE group at Microsoft Research. He joined Microsoft in 2006, before that he was 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 Lean, Z3, Yices 1.0 and SAL. Lean is a new open source theorem prover. Z3 and Yices are SMT solvers, and SAL (the Symbolic Analysis Laboratory) is an open source tool suite that includes symbolic and bounded model checkers, and automatic test generators. Z3 has been open sourced (under the MIT license) in the beginning of 2015. Leonardo received the Haifa Verification Conference Award in 2010. In 2014, the TACAS conference (Tools and Algorithms for the Construction and Analysis of Systems) has given an award for “The most influential tool paper in the first 20 years of TACAS” to his paper “Z3: An Efficient SMT Solver”. In 2015, Z3 received the Programming Languages Software Award from the ACM SIGPLAN.