Contact Phone: +49 721 60847401 Email:
Bitte warten... 
IPD Prof. Snelting Room 022, Building 50.34 Am Fasanengarten 5 76131 Karlsruhe Germany 
Consultation Hours: Montag & Dienstag 
Research interests
Interactive Theorem Provers, Type Theory, Category Theory, Homotopy Type Theory
Courses
 Lecture: Programming Paradigms , Wintersemester 2023/2024
 Common Excercises: Programming Paradigms  Exercises , Wintersemester 2023/2024
 Lecture: Programming Paradigms , Wintersemester 2022/2023
 Common Excercises: Programming Paradigms  Exercises , Wintersemester 2022/2023, Beste Übung
 Laboratory: Theorem prover lab: applications in programming languages , Sommersemester 2022
 Lecture: Programming Paradigms , Wintersemester 2021/2022
 Common Excercises: Programming Paradigms  Exercises , Wintersemester 2021/2022, Beste Übung
 Laboratory: Theorem prover lab: applications in programming languages , Sommersemester 2021
 Laboratory: PSE: Visualisation of Type Inference , Wintersemester 2020/2021
Publications
2020

Higher Inductive Types, Inductive Families, and InductiveInductive Types
February 2020 : J. v. Raumer 
A Syntax for Mutual Inductive Families
5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29July 6, 2020, Paris, France (Virtual Conference) 2020, pp. 23:123:21 : A. Kaposi, J. v. Raumer 
Coherence via WellFoundedness: Taming SetQuotients in Homotopy Type
Theory
LICS '20: 35th Annual {ACM/IEEE} Symposium on Logic in Computer Science, Saarbr{\"U}cken, Germany, July 811, 2020 2020, pp. 662675 : N. Kraus, J. v. Raumer
2019

Path Spaces of Higher Inductive Types in Homotopy Type Theory
34th Annual {ACM/IEEE} Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 2427, 2019 2019, pp. 113 : N. Kraus, J. v. Raumer
2017

Homotopy Type Theory in Lean
Interactive Theorem Proving  8th International Conference, ITP 2017, Bras{\'{\i}}lia, Brazil, September 2629, 2017, Proceedings 2017, pp. 479495 : F. v. Doorn, J. v. Raumer, U. Buchholtz
2016

Formalizing Double Groupoids and Cross Modules in the Lean Theorem
Prover
Mathematical Software  ICMS 2016  5th International Conference, Berlin, Germany, July 1114, 2016, Proceedings 2016, pp. 2833 : J. v. Raumer
2015

The Lean Theorem Prover (System Description)
Automated Deduction  {CADE25}  25th International Conference on Automated Deduction, Berlin, Germany, August 17, 2015, Proceedings 2015, pp. 378388 : L. M. d. Moura, S. Kong, J. Avigad, F. v. Doorn, J. v. Raumer
Advised thesis projects
finished
 Hammers for Lean 4 with usage of SMT solvers for HOL, Research project
 Interactive term rewriting for the Lean 4 theorem prover, Bachelor/Master thesis