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
- 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”
Supervised Theses
- Extending the multiset library in Isabelle/HOL
- A Modular Verification of Ordered Resolution in Isabelle/HOL
- Automating Proof Assistants with Hammers. A Comparative Study using Isabelle and Coq
- Syntax Highlighting in Isabelle (aka. Dark Mode for Isabelle/JEdit)
- Visualisation of an algorithm for solving the word problem in context-sensitive languages
- Function Existences in Isabelle
- Visualisation of an alternative CYK algorithm
Blog posts
Artikelaktionen