A tutorial on Lean is scheduled as associated event of the [44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL)] (http://conf.researchr.org/home/POPL-2017), which will take place in Paris at 16 January 2017.
Lean is a new open source theorem prover being developed at Microsoft Research, Carnegie Mellon University, and University of Washington. Lean is a new theorem prover that 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. The goal is to support both reasoning about complex systems and mathematical reasoning, and to verify claims in both domains.
The purpose of the tutorial is to help participants to get acquainted with Lean, and extend it using its meta programming capabilities. The tutorial is divided in three parts: introduction, advanced features, and writing and debugging tactics.
In the second part, we cover advanced features. It includes topics such as: type classes, implicit coercions, overloading, code extraction, and an introduction to the tactic framework. All the material is available online, and participants can access it before and after the tutorial.
In the final part, we describe how to write and debug non trivial tactics. Lean tactics and other meta programs are implemented using the same language used to write definitions and prove lemmas. The material is based on the book Programming in Lean. We will describe how to use and extend the Lean simplifier. We will also provide a short introduction to a resolution prover implemented in Lean.