Manuel Eberl

Name:	Manuel Eberl  [ˈmaːnu̯ɛl ˈeːbɐl]
Email:	<last name + m>@in.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 Decem­ber 2014, I am a PhD stu­dent in Com­pu­ter Sci­ence at the Chair for Lo­gic and Ver­i­fi­ca­tion. Since 2018, I am also an ed­itor of the Archive of Formal Proofs.

I mainly work on the for­mal­i­sa­tion of pure math­e­mat­ics in Isa­belle/­HOL. I be­lieve that the form­al­isa­tion of a sig­ni­fic­ant por­tion of known math­em­at­ics is a feas­ible and worth­while en­deav­our.

My cur­rent work is the form­al­isa­tion of the (semi-)auto­mat­ic solv­ing and veri­fic­a­tion of cer­tain classes of math­em­at­ic­al prob­lems, par­tic­u­larly those of the asymp­tot­ics of real-val­ued func­tions.

Mathematical Interests

With vary­ing levels of pro­fi­ciency:

• Com­plex ana­lysis
• Dis­crete math­em­at­ics, com­plex­ity ana­lysis, ana­lytic com­bin­at­or­ics, ana­lytic number the­ory
• Ab­stract al­gebra and cat­egory the­ory
• So­cial choice the­ory
• De­cision pro­ced­ures
• Pro­gram­ming lan­guages, func­tional pro­gram­ming, type sys­tems, and pro­gram veri­fic­a­tion

Current Work

• Analysis of Randomised Algorithms and Data Structures
• Semi-Automatic Real Asymptotics in Isabelle/HOL
• Formalisation of Tom Apostol's Introduction to Analytic Number Theory
• Continued Fractions

Drafts

• [PDF] [BibTeX]

  Manuel Eberl
  Nine Chapters of Analytic Number Theory in Isabelle/HOL
  

• [PDF] [BibTeX]

  Manuel Eberl
  Verified Real Asymptotics in Isabelle/HOL
  

Publications

• [PDF] [BibTeX]

  Manuel Eberl
  Verified Solving and Asymptotics of Linear Recurrences
  In: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (2019)

• [PDF] [BibTeX]

  Manuel Eberl, Max Haslbeck, and Tobias Nipkow
  Analysis of Random Trees
  In: Proceedings of the 9th International Conference on Interactive Theorem Proving (2018)

• [PDF] [BibTeX]

  Florian Brandl, Felix Brandt, Manuel Eberl, and Christian Geist
  Prov­ing the In­com­pat­ib­il­ity of Ef­fi­ciency and Strategy­proof­ness via SMT Solv­ing
  In: Journal of the ACM (2018)
  

  (The final publication is available at ACM)

• [PDF] [BibTeX]

  Manuel Eberl
  Prov­ing Di­vide and Con­quer Com­plex­it­ies in Isa­belle/­HOL
  In: Journal of Auto­mated Reas­on­ing (2016)
  

  (The final publication is available at link.springer.com)

• [PDF] [BibTeX]

  Manuel Eberl, Johannes Hölzl, and Tobias Nipkow
  A Ver­i­fied Com­piler for Prob­a­bil­ity Den­sity Func­tions
  In: Pro­ceed­ings of the 2015 Eu­ro­pean Sym­po­sium on Pro­gram­ming (2015)
  

  (The final publication is available at link.springer.com)

• [PDF] [BibTeX]
  Manuel Eberl
  A De­ci­sion Pro­ce­dure for Uni­vari­ate Real Poly­no­mi­als in Isa­belle/​HOL
  In: Pro­ceed­ings of the 2015 Con­fer­ence on Cer­ti­fied Pro­grams and Proofs (2015)
  

  (The final publication is available at ACM)

Theses

• A Formal Proof of the In­com­pat­ib­il­ity of SD-Ef­fi­ciency and SD-Strategy-Proof­ness
  Bach­e­lor’s The­sis in Math­em­at­ics at Tech­ni­sche Uni­ver­si­tät Mün­chen. 2016.
• A Ver­i­fied Com­piler for Prob­a­bil­ity Den­sity Func­tions
  Mas­ter’s The­sis in Computer Science at Tech­ni­sche Uni­ver­si­tät Mün­chen. 2014.
• Ef­fi­cient and Ver­i­fied Com­pu­ta­tion of Sim­u­la­tion Pre­orders on NFAs
  Bach­e­lor’s The­sis in Computer Science at Tech­ni­sche Uni­ver­si­tät Mün­chen. 2012.

Isabelle Formalisation Projects

See my separate list of formalisations projects.

Teaching

• Winter 17/18: co-or­gan­iser of the Func­tional Data Struc­tures Sem­inar and the practical course Spe­cific­a­tion and Veri­fic­a­tion
• Summer 16: co-or­gan­iser of the De­cision Pro­ced­ures sem­inar
• Winter 14/15: tu­to­rial (co-)su­per­vi­sor and proud Mas­ter of Com­pe­ti­tion (Jr) of In­tro­duc­tion to Func­tional Pro­gram­ming

Random stuff I made

• A small Haskell-based text snippet pasting service with Isa­belle high­light­ing
• A very small (∼250 LOC not counting GUI), on­line in­ter­ac­tive ray trac­ing demo in Java (with com­mented source code) that il­lus­trates the process of ray trac­ing. I made this when I was a BSc student and it fills me with nostalgia, so I leave it on here.
• Speaking of nostalgia: A raytracer in Java that I wrote as an en­try to a uni­ver­sity cod­ing con­test in my first semester. This won me a nice graph­ics card. ☺

Personal Interests

• Learn­ing lan­guages, lin­guist­ics, and phon­et­ics
• In par­tic­u­lar: learn­ing and speak­ing Es­per­anto (bon­volu kon­tak­ti min se vi vo­las pa­ro­li Es­pe­ran­ton kun mi)
• Bouldering and climbing
• Play­ing the ac­cor­dion and the low whistle

Recommended links

• The website of Isabelle, the In­ter­ac­tive The­o­rem Prover with which I work
• Probably the best place to learn Haskell, modulo gram­mar
• A web cartoon every stu­dent should know. And prob­a­bly ev­ery­one who works at a uni­ver­sity as well.
• ‘English is not normal’ – On why Eng­lish is the strange lan­guage that it is today.