|
|
|
Contact Phone: +49 721 608-47401 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 Inductive-Inductive 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 29-July 6, 2020, Paris, France (Virtual Conference) 2020, pp. 23:1--23:21 : A. Kaposi, J. v. Raumer -
Coherence via Well-Foundedness: Taming Set-Quotients in Homotopy Type
Theory
LICS '20: 35th Annual {ACM/IEEE} Symposium on Logic in Computer Science, Saarbr{\"U}cken, Germany, July 8-11, 2020 2020, pp. 662--675 : 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 24-27, 2019 2019, pp. 1--13 : N. Kraus, J. v. Raumer
2017
-
Homotopy Type Theory in Lean
Interactive Theorem Proving - 8th International Conference, ITP 2017, Bras{\'{\i}}lia, Brazil, September 26-29, 2017, Proceedings 2017, pp. 479--495 : 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 11-14, 2016, Proceedings 2016, pp. 28--33 : J. v. Raumer
2015
-
The Lean Theorem Prover (System Description)
Automated Deduction - {CADE-25} - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 2015, pp. 378--388 : L. M. d. Moura, S. Kong, J. Avigad, F. v. Doorn, J. v. Raumer
Advised thesis projects
open
- String Diagrams for Lean 4, masters thesis
running
- 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