Towards Lean 4: An Optimized Object Model for an Interactive Theorem Prover

Swiss LLVM Compiler and Code Generation Social! Talk about Compilers, Code Generation, and Programming Languages.

Tech Talk:

Lean 4, the next version of the Lean theorem prover, will move most of its frontend code from C++ to Lean itself. To ensure that the resulting code is reasonably efficient, Lean 4 will feature a new code generation backend together with a new object and memory management model. In this talk, I will discuss the general and ITP-specific constraints, such as performance, language interoperability, and startup time, that led us to this model and how we are planning to solve them with it.

Speaker:

Sebastian Ullrich is a second-year PhD student at Gregor Snelting's programming paradigms group at the Karlsruhe Institute of Technology (KIT). He is working on the Lean theorem prover together with Leonardo de Moura (Microsoft Research). Sebastian's research interests are program verification, the design of interactive theorem proving frontends, and macro expansion.

Where:

ETH Zurich, CAB, E72

http://www.rauminfo.ethz.ch/Rauminfo/grundrissplan.gif?gebaeude=CAB&geschoss=E&raumNr=72&

The building closes at 19:00. If you are late, you need to write us to be let in.

What is LLVM:

LLVM (http://www.llvm.org/) is an open source project that provides a collection of modular compiler and toolchain technologies. It is centered around a modern SSA-based compiler around which an entire ecosystem of compiler technology was developed. Most well know is the clang C++ compiler, which is e.g. used to deploy iOS. Beyond this a diverse set of projects is developed under the umbrella of LLVM. These include code generators and assemblers for various interesting architectures, a jit compiler, a debugger, run-time libraries (C++ Standard Library, OpenMP, Opencl library), program sanity checkers, and many more. LLVM has itself grown out of a research project more than 10 years ago and is the base of many exciting research projects today:

https://scholar.google.ch/scholar?cites=7792455789532680075&as_sdt=2005&sciodt=0,5&hl=de

Contact:

Tobias Grosser (https://www.inf.ethz.ch/personal/tgrosser/)