[cfe-dev] LLVM Compiler Social, Towards Lean 4 -- An Optimized Object Model for an Interactive Theorem Prover (Wednesday 12th)

[Tobias Grosser via cfe-dev]

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