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

I did a BSc and MSc in Computer Science and a BSc in Mathematics at the TU Munich. Afterwards, I did a PhD at the *Chair for Logic and Verification* under Tobias Nipkow. Since 2021, I now work there as a postdoc.

Since 2018, I am also an editor of the *Archive of Formal Proofs*.

I mainly work on the formalisation of pure mathematics and analysis of algorithms 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

### Books

*Functional Algorithms, Verified!*

by Tobias Nipkow, Jasmin Blanchette, Manuel Eberl, Alejandro Gómez-Londoño, Peter Lammich, Christian Sternagel, Simon Wimmer, Bohua Zhan

### 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*

PhD thesis at the*Technical University of Munich*(2021)*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

- Summer 21: organiser of the Functional Pearls seminar
- 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 both Isabelle and the subject of programming language semantics
- Another free Isabelle-related textbook, Functional Algorithms, Verified! by Nipkow
*et al*. This one includes a chapter on median-of-medians selection by me. - 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.