Balazs Toth

I'm a PhD student in Theoretical Computer Science and Theorem Proving at LMU Munich under the supervision of Jasmin Blanchette. My research focuses on interactive theorem proving, particularly on formalizing logical calculi in Isabelle. 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>@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

Talks

  • Adding Sorts to an Isabelle Formalization of Superposition (CPP 2026) Slides

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

WS 2025/26

SS 2025

WS 2024/25

SS 2024

WS 2023/24

  • Teaching assistant for "Einführung in die Programmierung"

Supervised Theses

  • Optimizing Pretty Print in Isabelle/VSCode - Lukas Ali Prokoph
  • Webview Panels for Isabelle: From Implementation to Unified Interfaces - Diana Korchmar
  • AI-assisted theorem search in Isabelle: A transformer-based approach - Fabian Kadlez
  • A Modular Verification of Ordered Resolution in Isabelle/HOL - Adnan Ahmed
  • Extending the multiset library in Isabelle/HOL - Yueying Xu
  • Automating Proof Assistants with Hammers. A Comparative Study using Isabelle and Coq - Mario Sögtrop
  • Syntax Highlighting in Isabelle (aka. Dark Mode for Isabelle/JEdit) - Kai Naumann
  • Visualisation of an algorithm for solving the word problem in context-sensitive languages - Samuel Delsol
  • Function Existences in Isabelle - David Schrank
  • Visualisation of an alternative CYK algorithm - Aahash Kevin Sundararuban

Blog posts

To top