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

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: Journal of Automated 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: Journal of the ACM (2018)
• Prov­ing Di­vide and Con­quer Com­plex­it­ies in Isa­belle/­HOL
  by Manuel Eberl
  In: Journal of Auto­mated Reas­on­ing (2016)

Conference Articles

• Verifying Randomised Social Choice
  by Manuel Eberl
  In: Proceedings of the 12th International Symposium on Frontiers of Combining Systems (2019)
• Nine Chapters of Analytic Number Theory in Isabelle/HOL
  by Manuel Eberl
  In: Proceedings of the 10th International Conference on Interactive Theorem Proving (2019)
• Verified Real Asymptotics in Isabelle/HOL
  by Manuel Eberl
  In: Proceedings of the 2019 International Symposium on Symbolic and Algebraic Computation
• Verified Solving and Asymptotics of Linear Recurrences
  by Manuel Eberl
  In: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (2019)
• Verified Analysis of Random Binary Tree Structures
  by Manuel Eberl, Max W. Haslbeck, and Tobias Nipkow
  In: Proceedings of the 9th International Conference on Interactive Theorem Proving (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: Pro­ceed­ings of the 2015 Eu­ro­pean Sym­po­sium on Pro­gram­ming
• A De­ci­sion Pro­ce­dure for Uni­vari­ate Real Poly­no­mi­als in Isa­belle/​HOL
  by Manuel Eberl
  In: Pro­ceed­ings of the 2015 Con­fer­ence on Cer­ti­fied Pro­grams and Proofs

Theses

• 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 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), online interactive 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
• Probably the best place to learn Haskell, modulo grammar
• 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.