Name: | Manuel Eberl [ˈmaːnu̯ɛl ˈʔeːbɐl] |
Email: | <firstname.lastname>@tum.de (German, English, Esperanto) |
PGP Key: | 0x9BE72A84.asc |
CV: | [PDF] |
ORCID: | 0000-0002-4263-6571 |
Scholarly profiles: | Google Scholar, DBLP |
Office: | MI 00.09.063 (by appointment) |
Phone: | +49 89 289-17328 |
Twitter: | @pruvisto |
Erdős number: | ≤ 4 |
About me
Since December 2014, I am a PhD student in Computer Science at the Chair for Logic and Verification. Since 2018, I am also an editor of the Archive of Formal Proofs.
I mainly work on the formalisation of pure mathematics in Isabelle/HOL. I believe that the formalisation of a significant portion of known mathematics is a feasible and worthwhile endeavour.
My current work is the formalisation of the (semi-)automatic solving and verification of certain classes of mathematical problems, particularly those of the asymptotics of real-valued functions.
Mathematical Interests
With varying levels of proficiency:
- Complex analysis
- Discrete mathematics, complexity analysis, analytic combinatorics, analytic number theory
- Abstract algebra and category theory
- Social choice theory
- Decision procedures
- Programming languages, functional programming, type systems, and program verification
Current Work
- Analysis of randomised algorithms and data structures
- Automating real and complex asymptotics in Isabelle/HOL
- Continued fractions
- Precise worst-case bounds for height-balanced trees
Journal Articles
- Verified Analysis of Random Binary Tree Structures (extended journal version)
by Manuel Eberl, Max W. Haslbeck, and Tobias Nipkow
In: J. Autom. Reasoning (2020) - Proving the Incompatibility of Efficiency and Strategyproofness via SMT Solving
by Florian Brandl, Felix Brandt, Manuel Eberl, and Christian Geist
In: J. ACM (2018) - Proving Divide and Conquer Complexities in Isabelle/HOL
by Manuel Eberl
In: J. Autom. Reasoning (2016)
Conference Articles
- Verified Textbook Algorithms. A Biased Survey (invited paper)
by Tobias Nipkow, Manuel Eberl, and Maximilian P. L. Haslbeck
In: Proceedings of ATVA 2020 - Verifying Randomised Social Choice
by Manuel Eberl
In: Proceedings of FroCoS 2019 - Nine Chapters of Analytic Number Theory in Isabelle/HOL
by Manuel Eberl
In: Proceedings of ITP 2019 - Verified Real Asymptotics in Isabelle/HOL
by Manuel Eberl
In: Proceedings of ISSAC 2019 - Verified Solving and Asymptotics of Linear Recurrences
by Manuel Eberl
In: Proceedings of CPP 2019 - Verified Analysis of Random Binary Tree Structures
by Manuel Eberl, Max W. Haslbeck, and Tobias Nipkow
In: Proceedings of ITP 2018 - A Verified Compiler for Probability Density Functions
by Manuel Eberl, Johannes Hölzl, and Tobias Nipkow
In: Proceedings of ESOP 2015 - A Decision Procedure for Univariate Real Polynomials in Isabelle/HOL
by Manuel Eberl
In: Proceedings of CPP 2015
Theses
- Asymptotic Reasoning in a Proof Assistant (draft)
PhD thesis at the Technical University of Munich (2020) - A Formal Proof of the Incompatibility of SD-Efficiency and SD-Strategy-Proofness
Bachelor's thesis at the Technical University of Munich (2016) - A Verified Compiler for Probability Density Functions
Master's thesis at the Technical University of Munich (2014) - Efficient and Verified Computation of Simulation Preorders on NFAs
Bachelor's thesis at the Technical University of Munich (2012)
Isabelle Formalisation Projects
See my separate list of formalisations projects.Teaching
- Winter 20/21: Master of Competition (Sr) for Functional Programming and Verification
- Winter 19/20: Master of Competition (Sr) for Functional Programming and Verification
- Summer 19: tutorial (co-)supervisor for Introduction to Theoretical Computer Science
- Winter 17/18: co-organiser of the Functional Data Structures Seminar and the practical course Specification and Verification
- Summer 16: co-organiser of the Decision Procedures seminar
- Winter 14/15: tutorial (co-)supervisor and proud Master of Competition (Jr) of Introduction to Functional Programming
Random stuff I made
- Cleaned-up versions of my team's winning solutions for the Proof Ground competition at ITP 2019.
- A small Haskell-based text snippet pasting service with Isabelle highlighting
- A very small (∼250 LOC not counting GUI), ray tracing demo in Java (with commented source code) that illustrates the process of ray tracing. I made this when I was a BSc student and it fills me with nostalgia, so I leave it on here.
Personal Interests
- Learning languages, linguistics, and phonetics
- In particular: learning and speaking Esperanto (bonvolu kontakti min se vi volas paroli Esperanton kun mi!)
- Bouldering and climbing
- Playing the accordion and the low whistle
Recommended links
- The website of Isabelle, the Interactive Theorem Prover with which I work
- The free Concrete Semantics book by Nipkow and Klein, which serves as a good introduction to Isabelle
- A nice introduction to Haskell
- A web cartoon every student should know. And probably everyone who works at a university as well.
- ‘English is not normal’ – On why English is the strange language that it is today.