Hello, I'm Lennard Gäher!

I am a fourth-year PhD student in Derek Dreyer's Foundations of Programming group at MPI-SWS, mainly working on the verification of (unsafe) Rust programs and libraries. My research interests include (program) verification, separation logics, and concurrency.

I obtained my Bachelor's degree from Saarland University in April 2020.

You can reach me at gaeher (ASCII 0x40) mpi-sws (ASCII 0x2E) org.

Github

Projects

RefinedRust: A Type System for High-Assurance Verification of Rust Programs, @ PLDI'24
Lennard Gäher, Michael Sammler, Ralf Jung, Robbert Krebbers, Derek Dreyer
Project Website
Talk at PLDI'24: slides recording
Talk at RW'23: slides
Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq, @ PLDI'24
Simon Spies, Lennard Gäher, Michael Sammler, Derek Dreyer
Project Website
Stuttering for Free, @ OOPSLA'23
Minki Cho, Youngju Song, Dongjae Lee, Lennard Gäher, Derek Dreyer
Later Credits: Resourceful Reasoning for the Later Modality, @ ICFP'22
Simon Spies, Lennard Gäher, Joseph Tassarotti, Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer
Project Website
Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations, @ POPL'22. Received Distinguished Paper award
Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, Derek Dreyer
Talk at POPL'22: slides, recording
Transfinite Iris: Resolving an Existential Dilemma of Step-Indexed Separation Logic @ PLDI'21
Simon Spies, Lennard Gäher, Daniel Gratzer, Joseph Tassarotti, Robbert Krebbers, Derek Dreyer, Lars Birkedal
Project Website
Mechanising Complexity Theory: The Cook-Levin Theorem in Coq @ ITP'21
Lennard Gäher, Fabian Kunze

Teaching experience

WS 21/22: Co-Teaching Assistant and Course Designer for Semantics (Core lecture) at Saarland University, together with Derek Dreyer and Simon Spies.
I developed large parts of the second half of the course, and mechanised most of the course material in the Coq proof assistant
for consumption by the students (amounting to several thousand lines of Coq code).
Additionally, I helped students with the course material, created exercises, and graded exercise sheets.
Received "Busy Beaver" teaching award by CS department
WS 20/21: Lecturer and Coach Mathematics Preparatory Course for incoming BSc computer science students at Saarland University
Together with another student, I prepared and delivered the lectures for one week of the course, attended by 150-200 students.
Additionally, I helped a group of ~10 students with the course material throughout the 4-week course in daily coaching sessions.
SS 20: Student TA for Introduction to Computational Logic (Core lecture) at Saarland University
WS 19/20: Student TA for Theoretical Computer Science (Base lecture) at Saarland University
SS 19: Student TA for Systems Architecture (Base lecture) at Saarland University
WS 18/19: Student TA for Programming I (Base lecture) at Saarland University
WS 17/18: Re-exam tutor for Programming I (Base lecture) at Saarland University