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

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
1 message Options
Reply | Threaded
Open this post in threaded view
|

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

Alberto Barbaro via llvm-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
_______________________________________________
LLVM Developers mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev