Tobias Grosser via llvm-dev
2018-Nov-28 13:13 UTC
[llvm-dev] LLVM Compiler Social, Towards Lean 4 -- An Optimized Object Model for an Interactive Theorem Prover (Wednesday 12th)
Dear all, WEDNESDAY 12th Dec, 19:00, we will have Sebastian Ullrich presenting on the Zurich LLVM Compiler Social: ======================================================================================Towards Lean 4: An Optimized Object Model for an Interactive Theorem Prover 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. 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. ====================================================================================== # Registration https://www.meetup.com/llvm-compiler-and-code-generation-socials-zurich/events/vxmqlqyxqbrb/ # What A social meetup to discuss compilation and code generation questions with a focus on LLVM, clang, Polly and related projects. Our primary focus is to provide a venue (and drinks & snacks) that enables free discussions between interested people without imposing an agenda/program. This is a great opportunity to informally discuss your own projects, get project ideas or just learn about what people at ETH and around Zurich are doing with LLVM. Related technical presentations held by participants are welcome (please contact us). # Who: - Anybody interested - - ETH students and staff - LLVM developers and enthusiasts external to ETH # When: 12.12.2018, 19:00 # Where: CAB E 72, ETH Zurich Best, Tobias