Export to
Tuesday, July 24, 2018 at 3:08pm.
Galois Tech Talk: The Lean Theorem Prover: Past, Present and Future
Galois is pleased to host the following tech talk. These talks are open to the interested public--please join us! (There is no need to pre-register for the talk.)
Website
Description
Abstract: Lean is an interactive theorem prover and functional programming language. Lean implements a version of the Calculus of Inductive Constructions. Its elaborator and unification algorithms are designed around the use of type classes, which support algebraic reasoning, programming abstractions, and other generally useful means of expression. Lean has parallel compilation and checking of proofs, and provides a server mode that supports a continuous compilation and rich user interaction in editing environments such as Visual Studio Code, Monaco, Emacs, and Vim. In the first part of this talk, we provide a short introduction to Lean, its applications, and its metaprogramming framework. We also describe how this framework extends Lean’s object language with an API to many of Lean’s internal structures and procedures, and provides ways of reflecting object-level expressions into the metalanguage. We provide evidence to show that our implementation is efficient, and that it provides a convenient and flexible way of writing not only metaprograms and small-scale interactive tactics, but also more substantial kinds of automation. In the second part, we describe our plans for the system, and what we are currently working on.
More information about Lean can be found at http://leanprover.github.io. The interactive book “Theorem Proving in Lean” is the standard reference for Lean. The book is available in PDF and HTML formats. In the HTML version, all examples and exercises can be executed in the reader’s web browser.
Bio: I’m a Principal Researcher in the RiSE group at Microsoft Research. I joined Microsoft in 2006, before that I was a Computer Scientist at SRI International. I obtained my PhD at PUC-Rio in 2000. My research areas are automated reasoning, theorem proving, decision procedures, SAT and SMT. I’m the main architect of Lean, Z3, Yices 1.0 and SAL. Lean is an open source theorem prover and programming language. Sebastian Ullrich and I are currently developing the next version (Lean 4). 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. I 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 the Z3 paper: Z3: An Efficient SMT Solver. 14th International Conference, TACAS 2008, vol. 4963 of Lecture Notes in Computer Science. In 2015, Z3 received the Programming Languages Software Award from ACM SIGPLAN. In 2017, the International Conference on Automated Deduction (CADE) presented the Skolem Award for my paper “Efficient E-Matching for SMT Solvers” that has passed the test of time, by being a most influential paper in the field. In 2018, the ETAPS conference has given the test of time award to the Z3 paper: Z3: An Efficient SMT Solver. You can see more about me at https://leodemoura.github.io/about.html