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

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