Contact

Tel	_	+49 681 302-2454
Mail	_
Room	_	429
Address	_	Saarland Informatics Campus Building E1 3 66123 Saarbrücken Germany
Github	_	NeuralCoder3
ORCID	_	0009-0006-0127-9623

Marcel Ullrich

About Me

• Curriculum Vitae (Outdated)

Research Interests

• dependently typed programming
• metaprogramming
• synthesis and constraint programming
• formal proof systems
• programming language design

Research Projects

• A MetaCoq plugin to generate induction principles for nested inductive types.
• Automatic differentiation in a functional higher-order intermediate representation using partial evaluation (see paper below)
• Formally verified translation validation in the presence of loops
• Low-level synthesis of sorting kernels (see paper below)
• Ongoing: Transpilation and Inter-language communication

Teaching

Advisor

• Master's Thesis: Automatic Differentiation of Memory and Affine Loops in AnyDSL, Christopher Jung (2022)
• Bachelor's Thesis: Teaching Program Semantics Interactively, Luise Puhl (2022, 2023)
• 3x HiWi Positions: Interactive Web Interpreter Programmer for Programming 2 Lecture Book (2022, 2023)
• Bachelor's Thesis: Reinforcement Learning in Program Synthesis: What makes it so powerful?, Florian Kneip (2023, 2024)
• Bachelor's Thesis: Building Factories using Z3, Joel Schnubel (2024 ongoing)
• HiWi Position: Equality Saturation in Compiler Optimizations (2025)
• If you are interested, take a look at our list of proposed topics or write me an e-mail

Lecturer's Assistant

• Programming 2 (SS2022)
• Seminar: Build an 8-bit Computer from Scratch (SS2022)
• Programming 2 (SS2023)
• Programming 1 (WS2023/24)
• Programming 2 (SS2025)
• Seminar: Equality Saturation (SS2025)
• Seminar: Build an 8-bit Computer from Scratch (SS2025)

Teaching Assistant

• Artificial Intelligence (SS2021)
• Grundzüge von Algorithmen und Datenstrukturen (WS2020/2021)
• Systemarchitektur (SS2020)
• Grundzüge der Theoretischen Informatik (WS2019/20)
• Introduction to Computational Logic (SS2019)
• Mathematik Vorkurs Dozent, Team, Organisator, Council (SS2019, SS2020, SS2021, SS2022, SS2023, SS2024, SS2025)
• Programmierung 1 (WS2018/19)

Publications

Journal Papers

• MimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age
  Leißa, R., Ullrich, M., Meyer, J. and Hack, S.
  Proc. ACM Program. Lang., 9 (POPL), 2025. [doi] [url] [bib]
  

  @article{Mimir:10.1145/3704840,
     author = {Lei\ss{}a, Roland and Ullrich, Marcel and Meyer, Joachim and Hack, Sebastian},
     title = {MimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age},
     year = {2025},
     issue_date = {January 2025},
     publisher = {Association for Computing Machinery},
     address = {New York, NY, USA},
     volume = {9},
     number = {POPL},
     url = {https://doi.org/10.1145/3704840},
     doi = {10.1145/3704840},
     abstract = {Traditional compilers, designed for optimizing low-level code, fall short when dealing with modern, computation-heavy applications like image processing, machine learning, or numerical simulations. We show that in all three studies, MimIR produces code that has state-of-the-art performance.},
     journal = {Proc. ACM Program. Lang.},
     month = jan,
     articleno = {4},
     numpages = {31},
     keywords = {compiler intermediate representations, dependent types, lambda-calculus}
   }

• Generating induction principles and subterm relations for inductive types using MetaCoq
  Liesnikov, B., Ullrich, M. and Forster, Y.
  CoRR, abs/2006.15135, 2020. [url] [bib]
  

  @article{DBLP:journals/corr/abs-2006-15135,
     author    = {Bohdan Liesnikov and Marcel Ullrich and Yannick Forster},
     title     = {Generating induction principles and subterm relations for inductive
                  types using MetaCoq},
     journal   = {CoRR},
     volume    = {abs/2006.15135},
     year      = {2020},
     url       = {https://arxiv.org/abs/2006.15135},
     eprinttype = {arXiv},
     eprint    = {2006.15135},
     timestamp = {Sat, 23 Jan 2021 01:12:25 +0100},
     biburl    = {https://dblp.org/rec/journals/corr/abs-2006-15135.bib},
     bibsource = {dblp computer science bibliography, https://dblp.org}
   }

Workshop Papers

• MimIrADe: Automatic Differentiation in MimIR
  Ullrich, M., Hack, S. and Leißa, R.
  Proceedings of the 34th ACM SIGPLAN International Conference on Compiler Construction, pages 70–80, Association for Computing Machinery, 2025. [doi] [url] [bib]
  

  @inproceedings{MimIrADe:10.1145/3708493.3712685,
     author = {Ullrich, Marcel and Hack, Sebastian and Lei\ss{}a, Roland},
     title = {MimIrADe: Automatic Differentiation in MimIR},
     year = {2025},
     isbn = {9798400714078},
     publisher = {Association for Computing Machinery},
     address = {New York, NY, USA},
     url = {https://doi.org/10.1145/3708493.3712685},
     doi = {10.1145/3708493.3712685},
     abstract = {Automatic Differentiation (AD) is at the core of all machine learning frameworks and has applications in scientific computing as well.
     Theoretical research on reverse-mode AD focuses on functional, higher-order languages, enabling AD to be formulated as a series of local, concise program rewrites.
     These theoretical approaches focus on correctness but disregard efficiency.
     Practical implementations, however, employ mutation and taping techniques to enhance efficiency.
     This approach, however, necessitates intricate, low-level, and non-local program transformations.
     In this work, we introduce MimIrADe, a functionally inspired AD technique implemented within a higher-order, graph-based ("sea of nodes") intermediate representation (IR).
     Our method consists of a streamlined implementation and incorporates standard optimizations, resulting in an efficient AD system.
     The higher-order nature of the IR enables us to utilize concise functional AD methods, expressing AD through local rewrites.
     This locality facilitates modular high-level extensions, such as matrix operations, in a straightforward manner.
     Additionally, the graph-based structure of the IR ensures that critical implementation aspects---particularly the handling of shared pullback invocations---are managed naturally and efficiently.
     Our AD pass supports a comprehensive set of features, including non-scalar types, pointers, and higher-order recursive functions.
     We demonstrate through standard benchmarks that a suite of common optimizations effectively eliminates the overhead typically associated with functional AD approaches, producing differentiated code that performs on par with leading mutation and taping techniques.
     At the same time, MimIrADe's implementation is an order of magnitude less complex compared to its contenders.},
     booktitle = {Proceedings of the 34th ACM SIGPLAN International Conference on Compiler Construction},
     pages = {70–80},
     numpages = {11},
     keywords = {automatic differentiation, functional programming, intermediate representation},
     location = {Las Vegas, NV, USA},
     series = {CC '25}
   }

• Synthesis of Sorting Kernels
  Ullrich, M. and Hack, S.
  Proceedings of the 23rd ACM/IEEE International Symposium on Code Generation and Optimization, pages 1–14, Association for Computing Machinery, 2025. [doi] [url] [bib]
  

  @inproceedings{Sorting:10.1145/3696443.3708954,
     author = {Ullrich, Marcel and Hack, Sebastian},
     title = {Synthesis of Sorting Kernels},
     year = {2025},
     isbn = {9798400712753},
     publisher = {Association for Computing Machinery},
     address = {New York, NY, USA},
     url = {https://doi.org/10.1145/3696443.3708954},
     doi = {10.1145/3696443.3708954},
     abstract = {Recently, AlphaDev has shown significant advances in the synthesis of branchless sorting kernels for arrays of lengths 3 to 5.                In this paper, we propose an enumerative search technique based on A* search and present novel optimality-pre­serving heuristics and non-optimality-preserving cuts for sorting kernel synthesis.                Our algorithm outperforms AlphaDev in synthesis time by two orders of magnitude ran on a standard notebook instead of a TPU cluster.                Because our algorithm can explore the solution space, we are able to enumerate all correct sorting kernels for length 3 and simply select the best-performing one.                For larger array lengths, we intelligently sample the solution space and find a sorting kernel that outperforms the state-of-the-art.                Furthermore, we establish a new tight lower bound for the shortest sorting kernel for length 4.                Finally, we provide a comprehensive comparison against several other existing synthesis techniques and show that none of them is able to synthesize sorting kernels for arrays longer than 3.},
     booktitle = {Proceedings of the 23rd ACM/IEEE International Symposium on Code Generation and Optimization},
     pages = {1–14},
     numpages = {14},
     keywords = {instruction-level optimizations, sorting kernels, super optimization, synthesis},
     location = {Las Vegas, NV, USA},
     series = {CGO '25}
   }

BSc Thesis

• Generating Induction Principles for Nested Inductive Types in MetaCoq
  Ullrich, M.
  B.Sc. Thesis, Saarland University, 2020. [pdf] [bib]
  

  @BACHELORSTHESIS{Ullrich:2020:BSc,
       author = { Marcel Ullrich},
       title = { {G}enerating {I}nduction {P}rinciples for {N}ested {I}nductive {T}ypes in {M}eta{C}oq },
       school = {Saarland University},
       year = { 2020 },
       month = {June},
       webpdf  = {https://www.ps.uni-saarland.de/~ullrich/bachelor/thesis.pdf},
       abstract = { },
   }