Manuel Eberl

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)
• Prov­ing the In­com­pat­ib­il­ity of Ef­fi­ciency and Strategy­proof­ness via SMT Solv­ing
  by Florian Brandl, Felix Brandt, Manuel Eberl, and Christian Geist
  In: J. ACM (2018)
• Prov­ing Di­vide and Con­quer Com­plex­it­ies in Isa­belle/­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 Ver­i­fied Com­piler for Prob­a­bil­ity Den­sity Func­tions
  by Manuel Eberl, Johannes Hölzl, and Tobias Nipkow
  In: Proceedings of ESOP 2015
• A De­ci­sion Pro­ce­dure for Uni­vari­ate Real Poly­no­mi­als in Isa­belle/​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 Func­tional Pro­gram­ming and Veri­fic­a­tion
• Winter 19/20: Master of Competition (Sr) for Func­tional Pro­gram­ming and Veri­fic­a­tion
• Summer 19: tutorial (co-)supervisor for Introduction to The­or­et­ical Com­puter Science
• Winter 17/18: co-organiser of the Func­tional Data Structures Seminar and the practical course Specification and Veri­fic­a­tion
• Summer 16: co-organiser of the Decision Procedures seminar
• Winter 14/15: tutorial (co-)supervisor and proud Master of Competition (Jr) of In­tro­duc­tion to Func­tional Pro­gram­ming

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.