[llvm-dev] Zurich LLVM Compiler Social, Tech-Talks: Compilers meet Isabelle & The Lean Theorem Prover (Thursday 13th)

Wed Sep 5 06:18:34 PDT 2018

Dear LLVM and compiler interested people,

next Thursday, 19:00, we will have two exciting tech-talks at the LLVM compiler social!

# The Lean Theorem Prover

Lean is a new theorem prover using dependent type theory (DTT). Lean 3 gained support for meta programming, employing dependent types not only as logic but also as a programming language. Lean as a programming language is used to implement tactics in Lean itself.

In this talk I want to give an overview of Lean, its meta programming framework, its (mathematical) library and current projects.

Bio: Johannes Hoelzl is since 2018 a postdoc at the VU Amsterdam working on the Matryoshka project and comaintaining Lean's mathematical library. In 2017, he did a postdoc with Jeremy Avigad (CMU). From 2009 to 2016 he was a PhD student and postdoc in Tobias Nipkow's Isabelle group at TU München. His main topic was Isabelle's analysis and probability theory. He, working with theorem provers since 2005.

# Compilers meet Isabelle

Abstract: Isabelle is an interactive proof assistant. Isabelle assists its users in writing functional programs and proofs about these and meticulously checks the proofs' correctness. This talk will consist of two parts. The first part will be a hands-on introduction to Isabelle, in which we develop an interpreter for a simple, Turing-complete programming language and verify a simple source-code transformation. The second part will outline what it takes to prove a compiler for a more realistic programming language correct.

Speakers: Dmitriy Traytel (1st part) and Andreas Lochbihler (2nd part)

Bio:

Dmitriy Traytel is a senior researcher in David Basin's information security group at ETH Zürich working on runtime verification and monitoring. He completed his PhD in 2015 in Tobias Nipkow's logic and verification group at TU München—the home of the Isabelle proof assistant. Dmitriy is both a developer and a user of Isabelle.

Andreas Lochbihler is a formal methods engineer at Digital Asset. From 2013 to 2018, Andreas was a senior researcher in the Information Security Group at ETH Zürich. His research revolved around the theory and tools to formalise protocols and their proofs such that definitions and proofs can be check mechanically. His framework CryptHOL brings to cryptography the expressiveness and rigour of higher-order logic and coalgebraic methods as implemented in the proof assistant Isabelle/HOL. Before joining ETH, he was a member of Programming Paradigms group at the Karlsruhe Institute of Technology and of the Sofware Systems group at the University of Passau. In his thesis, he built a formal model of Java concurrency which formalises source code, bytecode, a virtual machine, the compiler and the Java memory model in Isabelle/HOL.

# Registration

https://www.meetup.com/llvm-compiler-and-code-generation-socials-zurich/events/cbffknyxlbmb/

# 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:  13.09.2018, 19:00

# Where: CAB E 72, ETH Zurich

# 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

Best,
Tobias