Emin Karayel

About me

I have a degree in mathematics from the Karlsruhe Institute of Technology with specialization in functional analysis and more than 20 years of experience as a software engineer in particular at Google.

Now, I am a PhD student at the Chair for Logic and Verification supervised by Prof. Nipkow. My focus is on the formalization of big data algorithms, in particular, (parallel) streaming algorithms and derandomization methods using Isabelle.

Publications

• Verification of the CVM Algorithm with a Functional Probabilistic Invariant by Emin Karayel, Seng Joe Watt, Derek Khu, Kuldeep S. Meel, Yong Kiam Tan Published in: 16th International Conference on Interactive Theorem Proving (ITP 2025), Leibniz int. proc. inform. 352, 34:1–34:20(2025)
  DOI: 10.4230/LIPIcs.ITP.2025.34
• Derandomization with Pseudorandomness by Emin Karayel
  Published in: Annals of Formalized Mathematics 1:57–102(2025)
  DOI: 10.46298/afm.13477
• An Embarrassingly Parallel Optimal-Space Cardinality Estimation Algorithm by Emin Karayel
  Published in: Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2023), Leibniz int. proc. inform. 275, 35:1–35:22(2023)
  DOI: 10.4230/LIPIcs.APPROX/RANDOM.2023.35
  Full version available on arXiv
• Formalization of Randomized Approximation Algorithms for Frequency Moments by Emin Karayel
  Published in: 13th International Conference on Interactive Theorem Proving (ITP 2022), Leibniz int. proc. inform. 237, 21:1–21:21(2022)
  DOI: 10.4230/LIPIcs.ITP.2022.21
• Strong eventual consistency of the collaborative editing framework WOOT by Emin Karayel and Edgar Gonzàlez
  Published in: Distributed Computing 35, 145-164(2022)
  DOI: 10.1007/s00446-021-00414-6
  

Supervised Projects/Theses

I had the opportunity to work with:

• Zixuan Fan: Rabin’s Closest Pair of Points Algorithm, (Practical Course at TUM, 2024)
• Niklas Krofta: Topological Groups, (BSc at TUM, 2024)
• Jakob Schulz: A verified functional implementation of the Schönhage-Strassen-Algorithm, (MSc at TUM, 2023)
• Maximilian Spitz: Gray Codes for Arbitrary Numeral Systems, (Practical Course at TUM, 2023)
• Nils Cremer: Verified Enumeration of Trees, (BSc at TUM, 2023)
• Paul Hofmeier: Verification of Combinatorial Algorithms, (BSc at TUM, 2022)

Contact