|
|
|
Kontakt Tel.: +49 721 608-47401 Email:
Loading... |
IPD Prof. Snelting Raum 022, Gebäude 50.34 Am Fasanengarten 5 76131 Karlsruhe Deutschland |
|
Sprechzeiten: Montag & Dienstag |
|
Arbeitsgebiete
Interaktive Theorembeweiser, Typentheorie, Kategorientheorie, Homotopietypentheorie
Lehre
- Vorlesung: Programmierparadigmen , Wintersemester 2023/2024
- Übung: Programmierparadigmen - Übungen , Wintersemester 2023/2024
- Vorlesung: Programmierparadigmen , Wintersemester 2022/2023
- Übung: Programmierparadigmen - Übungen , Wintersemester 2022/2023, Beste Übung
- Praktikum: Theorembeweiserpraktikum: Anwendungen in der Sprachtechnologie , Sommersemester 2022
- Vorlesung: Programmierparadigmen , Wintersemester 2021/2022
- Übung: Programmierparadigmen - Übungen , Wintersemester 2021/2022, Beste Übung
- Praktikum: Theorembeweiserpraktikum: Anwendungen in der Sprachtechnologie , Sommersemester 2021
- Praktikum: PSE: Visualisierung von Typinferenz , Wintersemester 2020/2021
Veröffentlichungen
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
Betreute Studien- und Abschlussarbeiten
abgeschlossen
- Hammer für Lean 4 unter Benutzung von SMT-Solvern für HOL, Praxis der Forschung
- Interaktives Term-Rewriting für Lean 4, Bachelor-/Masterarbeit