Balazs Toth

I’m a PhD student in Theoretical Computer Science and Theorem Proving at LMU Munich under the supervision of Jasmin Blanchette. I’m interested in interactive theorem proving, particularly verifications in Isabelle including logic calculi. I’m also interested in programming languages, functional programming, type systems and mobile development.

You can send me email at <my first name>.<my last name>@ifi.lmu.de. I speak German and English. Please feel free to address me by my first name and, in German, to use “du” instead of “Sie”. My pronouns are he/him.

My office is room L 101, Oettingenstraße 67.

Publications

• A Modular Formalization of Superposition in Isabelle/HOL (Paper) (AFP Entry)

• Real-Time Double-Ended Queue Verified (Paper) (AFP Entry)

• AFP Entries

Theses

• Master: Arrays in Isabelle
• Bachelor: Object Detection in Resource-Constrained Mobile Environments
• Bachelor Sociology: Programmierparadigmen als Werkzeuge der Mustererkennung in sozialen Strukturen und Dynamiken

Teaching

SS 2025

• Teaching assistant for Logik und Diskrete Strukturen

WS 2024

• Teaching assistant for Einführung in die Programmierung

SS 2024

• Teaching assistant for Logik und Diskrete Strukturen
• Teaching assistant for Interactive Theorem Proving

WS 2023

• Teaching assistant for “Einführung in die Programmierung”

Blog posts

• Restricted TextFields In SwiftUI – A Reusable Implementation
• Snapshot Testing in Kotlin
• Sealed Interfaces
• Non-Empty Lists
• Testing MVI-ViewModels